coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
- To: Koper <Koper AT acn.waw.pl>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Coq equality-related problem.
- Date: Thu, 16 Sep 2004 16:41:29 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
It seems that you need Streicher's axiom K in order to achieve this. It has been proved for decidable types in the standard library Eqdep_dec for types with decidable equality.
The script below contains a proof of the uniquenes of derivations in your modelisation of lambda calculus under the hypothesis that equality is decidable on variables and function symbols.
Still I wonder if there's a simpler way to do it.
Require Import List.
Require Import Eqdep_dec.
Set Implicit Arguments.
Variable BaseType : Set.
Implicit Types a b c : BaseType.
Hypothesis eq_dec_BaseType : forall a b, {a=b} + {a<>b}.
Inductive SimpleType : Set :=
| BasicType(T: BaseType)
| ArrowType(A B : SimpleType).
Notation "x --> y" := (ArrowType x y) (at level 55, right associativity) : type_scope.
Notation "# x " := (BasicType x) (at level 0) : type_scope.
Implicit Types A B C : SimpleType.
Lemma eq_dec_SimpleType : forall A B, {A = B} + {A <> B}.
decide equality.
apply eq_dec_BaseType.
Qed.
Variable FunctionSymbol : Set.
Implicit Types f g h : FunctionSymbol.
Hypothesis eq_dec_FunctionSymbol : forall (f g: FunctionSymbol), {f=g} + {f<>g}.
Variable f_type: FunctionSymbol -> SimpleType.
Definition Env := list (option SimpleType).
Definition EmptyEnv : Env := nil.
Implicit Type x y : nat.
Implicit Type E : Env.
Definition VarD E x A := nth_error E x = Some (Some A).
Notation "E |= x := A" := (VarD E x A) (at level 60).
Lemma VarD_unique : forall E x A (v1 v2 : VarD E x A), v1 = v2.
unfold VarD; intros; generalize v1 v2; rewrite v1.
intros; apply K_dec_set; [idtac | pattern v0; apply K_dec_set]; auto;
decide equality; generalize a o; decide equality; apply eq_dec_SimpleType.
Qed.
Definition VarUD E x := nth_error E x = None \/ nth_error E x = Some None.
Notation "E |= x :!" := (VarUD E x) (at level 60).
Definition decl A E := Some A::E.
Definition declDummy E := None::E.
Inductive Preterm : Set :=
| Var(x: nat)
| Fun(f: FunctionSymbol)
| Abs(A: SimpleType)(M: Preterm)
| App(M N: Preterm).
Implicit Type Pt : Preterm.
Notation "^ f" := (Fun f) (at level 20).
Notation "% x" := (Var x) (at level 20).
Infix "@@" := App (at level 25, left associativity).
Notation "s [ x ]" := (s @@ x) (at level 30).
Notation "s [ x , y ]" := (s @@ x @@ y) (at level 30).
Notation " A ==> M" := (Abs A M) (at level 35).
Reserved Notation "E |- Pt := A" (at level 60).
Inductive Typing : Env -> Preterm -> SimpleType -> Set :=
| TVar: forall E x A, (E |= x := A) -> (E |- %x := A)
| TFun: forall E f, (E |- ^f := f_type f)
| TAbs: forall E A B Pt, (decl A E |- Pt := B) -> (E |- A ==> Pt := A --> B)
| TApp: forall E A B Pt0 Pt1,
(E |- Pt0 := A --> B) ->
(E |- Pt1 := A) ->
(E |- Pt0 @@ Pt1 := B)
where "E |- Pt := A" := (Typing E Pt A).
Record Term : Set := buildT {
env: Env;
term: Preterm;
type: SimpleType;
typing: Typing env term type
}.
Implicit Types M N : Term.
Lemma eq_dec_Preterm : forall (a b : Preterm), {a = b} + {a <> b}.
decide equality.
generalize x x0; decide equality.
generalize f f0; apply eq_dec_FunctionSymbol.
generalize A A0; apply eq_dec_SimpleType.
Qed.
Lemma eq_dec_Env : forall (a b : Env), {a = b} + {a <> b}.
decide equality; generalize a o; decide equality; apply eq_dec_SimpleType.
Qed.
Lemma eq_dec_EPS : forall (a b : Env * Preterm * SimpleType), {a = b} + {a <> b}.
decide equality.
apply eq_dec_SimpleType.
generalize a p; decide equality.
apply eq_dec_Preterm.
apply eq_dec_Env.
Qed.
Lemma Type_unique : forall t e T1 T2 (d1 : Typing e t T1) (d2 : Typing e t T2), T1=T2.
induction t; intros; inversion d1; inversion d2; trivial.
unfold VarD in *.
assert(Some (Some T1) = Some (Some T2)).
transitivity (nth_error e x); auto.
injection H7; trivial.
rewrite(@IHt _ _ _ H3 H8); auto.
set(e0 := IHt1 _ _ _ H2 H8); injection e0; auto.
Qed.
Lemma Deriv_unique : forall e t T (d1 d2 : Typing e t T), d1=d2.
refine(
fix Deriv_unique e t T (d1 d2 : Typing e t T) {struct d1 } : d1 = d2 :=
match d1 as d1' in Typing e1 t1 T1, d2 as d2' in Typing e2 t2 T2 return
forall (cast : (e1,t1,T1) = (e2,t2,T2)), (e1,t1,T1) = (e,t,T) ->
eq_rect (e1,t1,T1) (fun etT => match etT with (e,t,T) => Typing e t T end) d1' _ cast = d2'
with
| TVar _ _ _ _, TVar _ _ _ _ => _
| TFun _ _, TFun _ _ => _
| TAbs _ _ _ _ _, TAbs _ _ _ _ _ => _
| TApp _ _ _ _ _ _ _, TApp _ _ _ _ _ _ _ => _
| _, _ => _
end (refl_equal _) (refl_equal _));
intros; destruct t; try discriminate;
try discriminate cast; try discriminate dis;
injection cast; intros; generalize cast; clear cast.
generalize v v0; clear v v0.
rewrite H0; rewrite H1; rewrite H2.
intros; pattern cast; apply (K_dec_set eq_dec_EPS).
rewrite (VarD_unique v v0); apply refl_equal.
rewrite H1; rewrite H2.
intros; pattern cast; apply (K_dec_set eq_dec_EPS); apply refl_equal.
generalize t1; clear t1.
rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H4.
intros; pattern cast; apply (K_dec_set eq_dec_EPS).
rewrite(Deriv_unique _ _ _ t0 t1); apply refl_equal.
generalize t2 t3; clear t2 t3.
rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H3.
intros t2 t3.
intros; pattern cast; apply (K_dec_set eq_dec_EPS).
set(e0 := Type_unique t0 t2); injection e0; intro H7.
generalize t2 t3; clear e0 t2 t3; rewrite <- H7.
intros; rewrite(Deriv_unique _ _ _ t0 t2); rewrite(Deriv_unique _ _ _ t1 t3);
apply refl_equal.
Qed.
Theorem deriv_uniq: forall M N, env M = env N -> term M = term N -> type M = type N -> M = N.
intros; destruct M; destruct N; simpl in *.
generalize typing0; clear typing0.
rewrite H; rewrite H0; rewrite H1.
intros.
rewrite(Deriv_unique typing0 typing1).
apply refl_equal.
Qed.
Lemma typing_uniq: forall M N, env M = env N -> term M = term N -> type M = type N.
intros; destruct M; destruct N; simpl in *.
generalize typing0; clear typing0.
rewrite H; rewrite H0; intros.
apply (Type_unique typing0 typing1).
Qed.
Lemma term_eq: forall M N, env M = env N -> term M = term N -> M = N.
intros; apply deriv_uniq; auto.
apply typing_uniq; auto.
Qed.
- Re: [Coq-Club] Coq equality-related problem., Roland Zumkeller
Archive powered by MhonArc 2.6.16.