Web Interface Use Case

Example of use of the web interface for building a proof: functions that distribute over max (\up) are monotonic.

imports
[+]
declarations
[+]
dummy
[+]
assumptions
[+]
goal
   [          ]

[ prove     ]
[ add proof ]

click on import +, select arithmetic

imports
    [ arithmetic ]
[+]
declarations
[+]
dummy
[+]
assumptions
[+]
goal
   [          ]

[ prove     ]
[ add proof ]

click on declarations +, type in:

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
[+]
goal
   [          ]

[ prove     ]
[ add proof ]

click on assumptions +, type in:

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [          ]

[ prove     ]
[ add proof ]

• error: type of x,y not specified
• add dummy annotation

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
    [ x,y \in R ]
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [          ]

[ prove     ]
[ add proof ]

type in goal

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
[ add proof ]

• click on "prove"; proof fail
• click on "add proof"

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  [ proof step ]
    | by cases
    | assertion
    | new goal
    | calculation
    | automatic
qed

select "new goal"

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [+]
  prove  [          ]
    [ proof step ]
  qed
qed

click on assume+; type in:

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
    [ proof step ]
  qed
qed

click on proof step, select calculation

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
        [          ]
    [    ] { [          ] }
    [+] [          ]
  qed
qed

type in first and last step

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
        [ f.x \le f.y ]
    [    ] { [          ] }
    [+] [ x \le y ]
  qed
qed

click on [+] to add first relation

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
        [ f.x \le f.y ]
    [ =  ] { [          ] }
        [ f.x \up f.y = f.y ]
    [    ] { [          ] }
    [+] [ x \le y ]
  qed
qed

type in comment

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
        [ f.x \le f.y ]
    [ =  ] { [ $\le$ to $\up$ ] }
        [ f.x \up f.y = f.y ]
    [    ] { [          ] }
    [+] [ x \le y ]
  qed
qed

next step

imports
    [ arithmetic ]
[+]
declarations
    [ f \in R \tfun R ]
[+]
dummy
[+]
assumptions
    [ distributivity ] [ \qforall{x,y}{}{ f.(x \up y) = f.x \up f.y } ]
[+]
goal
   [ \qforall{x,y}{x \le y}{f.x \le f.y} ]

[ prove     ]
proof
  suffices
  assume [ NEW VARIABLES x,y ]
         [+]
  prove  [ x \le y \1\implies f.x \le f.y ]
        [ f.x \le f.y ]
    [ =  ] { [ $\le$ to $\up$ ] }
        [ f.x \up f.y = f.y ]
    [ =  ] { [ distributivity ] }
        [ f.(x \up y) = f.y ]
    [    ] { [          ] }
    [+] [ x \le y ]
  qed
qed

and so on