(******************************************************************************) (*** Chantal Keller ***) (*** D'après l'article "Intuitionistic Model Constructions and ***) (*** and Normalization Proofs" de Thierry Coquand et Peter Dybjer, partie 2 ***) (******************************************************************************) Set Implicit Arguments. (* Types et termes *) Section Syntax. Inductive type : Set := | N : type | Arrow : type -> type -> type. Notation " a '-->' b " := (Arrow a b) (at level 60, right associativity). Inductive term : type -> Set := | K : forall A B: type, term (A --> B --> A) | S : forall A B C: type, term ((A --> B --> C) --> (A --> B) --> A --> C) | app : forall (A B: type) (c: term (A --> B)) (a: term A), term B | o : term N | s : forall a: term N, term N | rec : forall (C: type) (d: term C) (e: term (N --> C --> C)), term (N --> C). End Syntax. Notation " a '-->' b " := (Arrow a b) (at level 60, right associativity). (* Relation de conversion *) Section Conversion. Inductive conversion : forall (A: type), term A -> term A -> Prop := | refl : forall (A: type) (a: term A), conversion a a | trans : forall (A: type) (a b c: term A), conversion a b -> conversion b c -> conversion a c | sym : forall (A: type) (a b: term A), conversion a b -> conversion b a | cong_app : forall (A B: type) (a b: term (A --> B)) (c d: term A), conversion a b -> conversion c d -> conversion (app a c) (app b d) | cong_s : forall (a b: term N), conversion a b -> conversion (s a) (s b) | cong_rec : forall (C: type) (d1 d2: term C) (e1 e2: term (N --> C --> C)), conversion d1 d2 -> conversion e1 e2 -> conversion (rec d1 e1) (rec d2 e2) | conv_K : forall (A B: type) (a: term A) (b: term B), conversion (app (app (K _ _) a) b) a | conv_S : forall (A B C: type) (g: term (A --> B --> C)) (f: term (A --> B)) (a: term A), conversion (app (app (app (S _ _ _) g) f) a) (app (app g a) (app f a)) | conv_rec_o : forall (C: type) (d: term C) (e: term (N --> C --> C)), conversion (app (rec d e) o) d | conv_rec_s : forall (C: type) (d: term C) (e: term (N --> C --> C)) (a: term N), conversion (app (rec d e) (s a)) (app (app e a) (app (rec d e) a)). End Conversion. Notation " a 'conv' b " := (conversion a b) (at level 60). Hint Resolve refl trans sym cong_app cong_s cong_rec conv_K conv_S conv_rec_o conv_rec_s : norm. (* Modèle standard *) Section Semantics. Fixpoint rec_op (C: Set) (d: C) (e: nat -> C -> C) (n: nat) {struct n} : C := match n with | O => d | Datatypes.S a => e a (rec_op d e a) end. Fixpoint int_type (t: type) : Set := match t with | N => nat | t1 --> t2 => (int_type t1) -> (int_type t2) end. Fixpoint int_term (A: type) (a: term A) {struct a} : int_type A := match a in term B return int_type B with | K _ _ => fun x y => x | S _ _ _ => fun g f x => g x (f x) | app _ _ c a => (int_term c) (int_term a) | o => O | s a => Datatypes.S (int_term a) | rec _ d e => rec_op (int_term d) (int_term e) end. Theorem th1 : forall (A: type) (a b: term A), a conv b -> int_term a = int_term b. Proof. intros A a b h. induction h; auto. transitivity (int_term b); auto. simpl; rewrite IHh1; rewrite IHh2; reflexivity. simpl; rewrite IHh; reflexivity. simpl; rewrite IHh1; rewrite IHh2; reflexivity. Qed. Lemma cor2 : o conv (s o) -> False. Proof. intro h. assert (0 = 1). change (int_term o = int_term (s o)). apply th1; trivial. discriminate H. Qed. End Semantics. (* Modèle non standard et algorithme de normalisation *) Section Normalization. Fixpoint int_type2 (t: type) : Set := match t with | N => nat | A --> B => ((term (A --> B)) * ((int_type2 A) -> (int_type2 B)))%type end. Fixpoint quoteN (x: nat) : term N := match x with | O => o | Datatypes.S y => s (quoteN y) end. Fixpoint quote (A: type) : int_type2 A -> term A := match A as X return int_type2 X -> term X with | N => quoteN | A --> B => fun x => let (c,_) := x in c end. Definition appM (A B: type) (x: int_type2 (A --> B)) (q: int_type2 A) : int_type2 B := let (_,f) := x in f q. Fixpoint int_term2 (A: type) (a: term A) {struct a} : int_type2 A := match a in term X return int_type2 X with | K _ _ => (K _ _, fun p => (app (K _ _) (quote _ p), fun q => p)) | S _ _ _ => (S _ _ _, fun p => (app (S _ _ _) (quote _ p), fun q => (app (app (S _ _ _) (quote _ p)) (quote _ q), fun r => appM (appM p r) (appM q r)))) | app _ _ c a => appM (int_term2 c) (int_term2 a) | o => O | s a => Datatypes.S (int_term2 a) | rec _ d e => (rec (quote _ (int_term2 d)) (quote _ (int_term2 e)), rec_op (int_term2 d) (fun x y => appM (appM (int_term2 e) x) y)) end. Definition nf (A: type) (a: term A) := quote _ (int_term2 a). Lemma th3_aux : forall (A: type) (a b: term A), a conv b -> int_term2 a = int_term2 b. Proof. intros A a b h. induction h; auto. transitivity (int_term2 b); auto. simpl; rewrite IHh1; rewrite IHh2; reflexivity. simpl; rewrite IHh; reflexivity. simpl; rewrite IHh1; rewrite IHh2; reflexivity. Qed. Theorem th3 : forall (A: type) (a b: term A), a conv b -> nf a = nf b. Proof. intros A a b h. unfold nf. rewrite (th3_aux h). reflexivity. Qed. Fixpoint Gl (A: type) : int_type2 A -> Prop := match A as X return int_type2 X -> Prop with | N => fun _ => True | A --> B => fun q => forall (p: int_type2 A), Gl A p -> Gl B (appM q p) /\ app (quote _ q) (quote _ p) conv quote _ (appM q p) end. Lemma lem5 : forall (A: type) (a: term A), Gl A (int_term2 a). Proof. intros A a. induction a; simpl. intros p h1. split; auto with norm. intros p h1. split; auto with norm. intros p0 h2. split; auto with norm. intros p1 h3. destruct (h1 p1 h3). destruct (h2 p1 h3). destruct (H (appM p0 p1) H1). split; auto. eapply trans. apply conv_S. eapply trans. apply cong_app. eexact H0. eexact H2. exact H4. simpl in IHa1. destruct (IHa1 (int_term2 a2) IHa2). exact H. exact I. exact I. intros p _. induction p; simpl; simpl in IHa2; split; auto with norm; destruct IHp; destruct (IHa2 p I); destruct (H1 (rec_op (int_term2 a1) (fun (x : nat) (y : int_type2 C) => appM (appM (int_term2 a2) x) y) p) H). exact H3. eapply trans. apply conv_rec_s. eapply trans. apply cong_app. apply refl. eexact H0. eapply trans. apply cong_app. eexact H2. apply refl. exact H4. Qed. Theorem th4 : forall (A: type) (a: term A), a conv (nf a). Proof. intros A a. induction a; auto with norm. eapply trans. apply cong_app; eauto. unfold nf; simpl. unfold appM; simpl. assert (Gl _ (int_term2 a1)). apply lem5. assert (Gl _ (int_term2 a2)). apply lem5. simpl in H. destruct (H (int_term2 a2) H0). exact H2. eapply trans. apply cong_s; eauto. simpl; auto with norm. eapply trans. apply cong_rec; eauto. unfold nf; simpl; auto with norm. Qed. Lemma co7 : forall (A: type) (a b: term A), a conv b <-> nf a = nf b. Proof. intros A a b. split. apply th3. intro h. eapply trans. apply th4. rewrite h. apply sym. apply th4. Qed. End Normalization.