# TP05: Dependent pattern matching and accessiblity predicate

# Dependent pattern-matching and the "injection" tactic

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

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) (A : 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 := ...

This page has been generated by coqdoc