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 3: summary

  • bool vs Prop
  • views as iff
  • using views
  • reflect and other inductive spec
  • a real proof

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 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 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

Motto: don't let Coq drive your proof!


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


Infinitude of primes



Lesson 3: 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
  • have: ... by ... forward step
  • rewrite ?rule