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.
Lesson 5 : summary
- bool vs Prop
- views as iff
- using views
- reflect and other inductive
spec
Propositions and booleans
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:
- structure to your proof as a tree
- more expressive logic (closed under forall, exists...)
Booleans:
- computation & Excluded Middle
- Uniqueness of Identity Proofs (lesson 4)
We want the best of the two worlds, and a way to
link them: views.
Stating and proving a reflection view
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.
Using views
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 predicate and other specs
The reflect inductive predicate has an index.
Indexes are replaced by the value dictated by the
constructor when performing a case 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
Using views with non reflexive lemmas
- By processing an assumption through a lemma.
- The leading / makes the lemma work as a function.
- If lemma states A -> B, we ca use it as a function to get a proof of B from a proof of A.
- One can also chain multiple views on the same stack item.
Using views with tactics
- we can also use views on non reflexive lemmas: apply/V, case/V.
The view mechanism can also be used for double implication:
- A <-> B is a notation for the conjonction: (A -> B) /\ (B -> A)
- If V is a proof of (A <-> B), apply/V will automatically guess which part of the conjonction it will use