(** * TP05 : Dependent pattern matching *) (* To build an html version of the TD sheet, use the command "coqdoc -utf8 --no-lib-name --no-index --lib-subtitles TP05.v" *) (************************************) (** * 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. **) 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 end. (** 4) Give now the proof term that says [Zero <> One]. **) Definition NonConf : Zero = One -> False := ...