Machine-Checked Mathematics

Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can save your edits inside your browser and load them back. Finally, you can download your working copy of the file, e.g., for sending it to teachers.

Exercise 1:

Extend the definitions introduced in Lesson 6, so that the proof of the test1 lemma succeeds without changing the proof script.

Exercise 2. We define a type tuple for polymorphic lists with a prescribed length, given as a parameter. This type is a dependent pair. This condition is expressed as a (boolean) constraint on the size of a list, coerced to Prop via the usual is_true coercion. The infix == notation refers to the notation available on instances of the eqType structure, as defined by the library loaded in this section. This structure is isomorphic to the one we used in Lesson 6. In particular, it is endowed with a reflection lemma eqP, relating the boolean test with equality.

Fill the missing parts so that the test lemmas are proved without changing their script.

About size.
About map.

Section Def.

Variables (n : nat) (T : Type).

Record tuple : Type := Tuple {tval : list T; valP : size tval == n}.

Coercion tval : tuple >-> list.

Lemma size_tuple (t : tuple) : size t = n.
(* Something goes here *)
 Proof. apply/eqP. apply: valP.
Qed.

End Def.

Canonical nil_tuple T := @Tuple 0 T [::] erefl.

Canonical cons_tuple n T x (t : tuple n T) :=
   Tuple (valP t : size (x :: t) == S n).

(* Something goes here, two things actually. *)

Section TupleTest.

Variable P : list nat -> Prop.
Variable hP : forall n, forall t : tuple (S n) nat, P t.

Lemma test2 : P (cons 2 nil).
Proof. apply: hP. Qed.

End TupleTest.

Section MapTuple.

Variables  (T1 T2 : Type) (n : nat) (f : T1 -> T2).

Lemma map_tupleP (t : tuple n T1) : size  (map f t) == n.
Proof.
(* Finish the proof, and may be more *)
  by rewrite size_map size_tuple.
Qed.
 Canonical map_tuple t := Tuple (map_tupleP t).

End MapTuple.

Section TupleTest.

Variable P : list bool -> Prop.
Variable hP : forall n, forall t : tuple (S n) bool, P t.

Lemma test3 (f : nat -> bool) : P (map f (cons 2 nil)).
Proof. apply: hP. Qed.

End TupleTest.