To play this document inside your browser use ALT-N and ALT-P.
You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.
spec
So far we used boolean connectives. But this is not what is used in the Curry Howard correspondence to represent connectives and their proofs.
Let's play a little with and and andb, or and orb in order to understand the difference.
Propositions:
This slide corresponds to section 3.x of the Mathematical Components book
To link a concept in bool and one in Prop we typically use the reflect predicate.
To prove reflect we use the iffP lemma that turns it into a double implication. This is also a recap of many of the proof commands we have seen so far.
The syntax /view can be put in intro patterns to modify the top assumption using view
The apply: tactic accepts a /view flag to modify the goal using view.
The case: tactic accepts a /view flag to modify the term being analyzed just before performing the case analysis.
The reflect inductive predicate has an index.
Indexes are replaced by the value dictated by the constructor when prforming a casa analysis. In a way indexes express equations that are substituted automatically.
In Mathematical Components we exploit this feature of the logic in order to structure proofs that proceed by case split.
Note that (andP _ _) has in the type, as the value of
the index, (_ && _) that we call a pattern
. The case:
tactic looks for a subterm of the goal that matches the
pattern and guesses
that the two _ are respectively
a and b. This form of automation is the same of rewrite.
One can craft many spec
to model the structure of a
proof. Eg leqP and ltngtP