Dependent pattern-matching and the "injection" tactic

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
• 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. 2) Write a concatenating function for this type by directly writing its term (i.e. without using the tactic mode). 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.