## Sunday, 30 November 2008

### Decidable Equality and Type Equality

`Require Import Eqdep_dec_defined.(** Same as Eqdep_dec but s/Qed/Defined/ **)Theorem dep_destruct :  forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),    (forall x' (v' : T' x') (Heq : x' = x),      P (match Heq in (_ = x) return (T' x) with           | refl_equal => v'         end)) ->      P v.  intros T T' x v P I; apply (I _ v (refl_equal _)).Defined.(** Stolen from http://www.cs.harvard.edu/~adamc/cpdt/ **)Inductive type : Set :=| Nat : type| Arrow : type -> type -> type.Definition eq_type_dec' (s t : type) : s = t \/ s <> t.decide equality.Defined.Inductive equand : type -> Set :=| Zero : equand Nat| Succ : equand (Arrow Nat Nat).Definition eq_equand_dec {T} (x y : equand T) : {x = y} + {x <> y}.intro.destruct x;  intro y; apply (dep_destruct type equand _ y);    intros T y' Teq; destruct y';      discriminate ||        rewrite <- (eq_proofs_unicity eq_type_dec' (refl_equal _) Teq).left; reflexivity.left; reflexivity.Defined.`