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

where

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

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.

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.

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

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.

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

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.

9) Define lt2 the lexicographic product of <.

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.

Operations on well founded relations

12) Prove the inversion lemma for Acc.

Sub-relation

13) Define relation inclusion.

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

Inverse image

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

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

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.

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

Lexicographic product

20) Define the lexicographic product of two relations.

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

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)