TP 5 : Dependent pattern matching and accessibility

Dependent pattern-matching

The most general form of pattern matching in Coq is
      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)
1) Define a type listn T n of lists of size n containing elements of type T. You can draw inspiration from Coq's type list.
2) Write a concatenating function for this type by directly writing its term (i.e. without using the tactic mode). You will need the full power of pattern matching.

The "injection" tactic

We want to see how the "injection" tactic works. Remember that "injection" is used to show injectivity of constructors of an inductive type: a term of an inductive type built with a constructor "c₁" cannot be equal to a term built with constructor "c₂" different from "c₁".
For simplicity we take an inductive type with 2 constructors.
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 := ...

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

4) Give now the proof term that says Zero <> One.
Definition NonConf : Zero = One -> False := ...

The Acc accessiblity predicate

In previous sessions, we used well-foundedness to prove properties and to define recursive functions. Let us now take a closer look at what it means: Print well_founded. returns
      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 _]
which means that a relation R : A -> A -> Prop is well founded if all its elements are accessible: forall a : A, Acc R a.
Being accessible is in turn defined by
      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
saying that if all predecessors of x by R are accessible, then x is accessible too.
5) How does the accessibility property start off?
When we want to prove Acc for an element x, we usually start by inspecting the shape of x (especially if A is inductive). With the shape of x, we know if R y x can hold or not.
Keep in mind that Acc is an inductive predicate, so you can always use induction on a proof of Acc x to prove another property.

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.

9) Define lt2 the lexicographic product of <.
Definition lt2 : relation (nat*nat) := ...

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.

Operations on well founded relations

12) Prove the inversion lemma for Acc.
Lemma Acc_inv : forall (A : Type) (R : relation A) x y, R x y -> Acc R y -> Acc R x.


13) Define relation inclusion.
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.

Inverse image

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.

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'.
End Inverse_image.

Transitive closure

17) Define the (non-reflexive) transitive closure operator.
18) Prove that if x is accessible by R then x is accessible from the transitive closure of x. You will need the lemma Acc_inv.
Lemma Acc_trans (A : Type) (R : relation A) :
  forall x, Acc R x -> Acc (trans R) x.

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.

Lexicographic product

20) Define the lexicographic product of two relations.
Definition lexprod (A B : Type) (RA : relation A) (RB : relation 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).

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