# tp5

# Dependent pattern-matching

match t as n in T return P with ...

- t is the term to be destructed
- n is a name used to refer to t (used when it is an application)
- T is the type of t, in case it contains terms that need to be bound for the matching branches (dependent types)
- P is the elimination predicate, the type of the matching branches (necessary when it differs between branches and cannot be infered)

# The "injection" tactic

Inductive Two : Set := Zero | One.

3) Define the elimination function of the equality type by directly
writing its term. This function takes proofs of P x and x = y
and returns a proof of P y.

Definition eq_elim (A : Type) (P : A -> Prop) (x y : A)

(Px : P x) (equality : x = y) : P y := ...

(Px : P x) (equality : x = y) : P y := ...

The crucial part for diff is "strong elimination" :
it allows building a type (here a Prop)
by pattern matching values from a small type like nat.

Definition diff (P Q : Prop) x : Prop :=

match x with

| Zero => P

| One => Q

end.

match x with

| Zero => P

| One => Q

end.

4) Give now the proof term that says Zero <> One.

Definition NonConf : Zero = One -> False := ...

# The Acc accessiblity predicate

well_founded =

fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a

: forall A : Type, (A -> A -> Prop) -> Prop

Argument A is implicit

Argument scopes are [type_scope _]

Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=

Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x

## First example: lt and its lexicographic product.

Require Import Relations.

Require Import Arith.

Require Import Omega.

The following line turn implicit all arguments that can be infered
from other arguments, this removing the need to explicitely tag
them with { }.

Set Implicit Arguments.

6) As an example, prove the lemmas Acc lt 0, Acc lt 1,
and Acc lt 2.
7) What is the structure of a proof of Acc lt n?
8) Prove (on paper) that any natural number is accessible by <.
Then (and only then), translate this proof to Coq.

Theorem lt_wf : well_founded lt.

Proof.

...

Qed.

Proof.

...

Qed.

9) Define lt2 the lexicographic product of <.

Definition lt2 : relation (nat*nat) := ...

Notation "x << y " := (lt2 x y) (at level 70).

Notation "x << y " := (lt2 x y) (at level 70).

10) Prove that lt2 is a strict order, i.e. is irreflexive and
transitive.
You can use SearchPattern or SearchAbout to look for lemmas
you might need about lt and le.
11) Prove (on paper) that the strict lexicographic ordering on
nat*nat is well-founded.
Then (and only then) translate this proof to Coq.

Lemma lt2_wf : well_founded lt2.

Proof.

...

Qed.

Proof.

...

Qed.

Lemma Acc_inv : forall (A : Type) (R : relation A) x y, R x y -> Acc R y -> Acc R x.

Proof.

...

Qed.

Proof.

...

Qed.

Definition rel_incl (A : Type) (R S : relation A) := ...

14) Prove that if R is included in S and S is well-founded,
then R is well-founded.

Theorem rel_incl_wf (A : Type) (R S : relation A) :

rel_incl R S -> well_founded S -> well_founded R.

Proof.

...

Qed.

rel_incl R S -> well_founded S -> well_founded R.

Proof.

...

Qed.

Section Inverse_image.

Variables (A B : Type) (R : relation B) (f : A -> B).

Definition R' x y := R (f x) (f y).

15) Prove the following lemma relating Acc R and Acc R'.

Lemma Acc_inverse_eq : forall y, Acc R y -> forall x, y = (f x) -> Acc R' x.

Proof.

...

Qed.

Proof.

...

Qed.

16) Deduce from this lemma that the reverse image of a well-founded
relation by any function is a well-founded relation.

Lemma wf_inverse_image : well_founded R -> well_founded R'.

Proof.

...

Qed.

End Inverse_image.

Proof.

...

Qed.

End Inverse_image.

### Transitive closure

Lemma Acc_trans (A : Type) (R : relation A) :

forall x, Acc R x -> Acc (trans R) x.

Proof.

...

Qed.

forall x, Acc R x -> Acc (trans R) x.

Proof.

...

Qed.

19) Prove that if R is well-founded, then its transitive closure
is well-founded.

Theorem wf_trans : forall (A : Type) (R : relation A),

well_founded R -> well_founded (trans R).

Proof. intros A R wfR x. apply Acc_trans. apply wfR. Qed.

well_founded R -> well_founded (trans R).

Proof. intros A R wfR x. apply Acc_trans. apply wfR. Qed.

Definition lexprod (A B : Type) (RA : relation A) (RB : relation B)

: relation (A*B) := ...

: relation (A*B) := ...

21) prove that the lexicographic product of two well-founded relations
is a well-founded relation.

Theorem lexprod_wf (A B : Type) (RA : relation A) (RB : relation B) :

well_founded RA -> well_founded RB -> well_founded (lexprod RA RB).

Proof.

...

Qed.

well_founded RA -> well_founded RB -> well_founded (lexprod RA RB).

Proof.

...

Qed.

22) Bonus: What about the dependent lexicographic product?
(i.e. when the type of the second component of the pair depends
on the value of the first component)

This page has been generated by coqdoc