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.

No comments: