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.


(notes)

This slide corresponds to section 3.x of the Mathematical Components book


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.

(notes)
This slide corresponds to sections 4.1.1 and 4.1.2 of the Mathematical Components book


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.


(notes)
This slide corresponds to sections 4.1.3 and 4.1.4 of the Mathematical Components book


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


(notes)
This slide corresponds to section 4.2 of the Mathematical Components book


Lesson 5: sum up

  • reflect and iffP
  • case/v: m case split + view application
  • move=> /v H introduction + view
  • apply/v: t backchain with a view
  • _spec predicates to model case split leqP and ifP
  • move=> [] (for case)
  • move=> -> (for rewrite)
  • ... => ... the arrow can be used after any command