Definition eqat (A B : atomic) : bool := match A, B with | Nat, Nat => true | Bool, Bool => true | _,_ => false end. Lemma eqatP : Equality.axiom eqat. Proof. by case=> [[|]|[|]]//=; constructor. Qed. Canonical Structure atomic_eqMixin := EqMixin eqatP. Print nat_eqType. Canonical Structure atomic_eqType := Eval hnf in (Equality.Pack atomic_eqMixin atomic). Fixpoint eqst (A B : ST) {struct A} : bool := match A , B with | Atomic a, Atomic b => a==b | A1 --> A2, B1 --> B2 => (eqst A1 B1) && eqst A2 B2 | A1 ** A2, B1 ** B2 => eqst A1 B1 && eqst A2 B2 | A1 +++ A2, B1 +++ B2 => eqst A1 B1 && eqst A2 B2 | _, _ => false end. Lemma eqst_arrow : forall b1 c1 b2 c2, eqst (b1 --> c1) (b2 --> c2) = eqst b1 b2 && eqst c1 c2. Proof. by move=> *. Qed. Lemma eqst_prod : forall b1 c1 b2 c2, eqst (b1 ** c1) (b2 ** c2) = eqst b1 b2 && eqst c1 c2. Definition eqat (A B : atomic) : bool := match A, B with | Nat, Nat => true | Bool, Bool => true | _,_ => false end. Lemma eqatP : Equality.axiom eqat. Proof. by case=> [[|]|[|]]//=; constructor. Qed. Canonical Structure atomic_eqMixin := EqMixin eqatP. Print nat_eqType. Canonical Structure atomic_eqType := Eval hnf in (Equality.Pack atomic_eqMixin atomic). Fixpoint eqst (A B : ST) {struct A} : bool := match A , B with | Atomic a, Atomic b => a==b | A1 --> A2, B1 --> B2 => (eqst A1 B1) && eqst A2 B2 | A1 ** A2, B1 ** B2 => eqst A1 B1 && eqst A2 B2 | A1 +++ A2, B1 +++ B2 => eqst A1 B1 && eqst A2 B2 | _, _ => false end. Lemma eqst_arrow : forall b1 c1 b2 c2, eqst (b1 --> c1) (b2 --> c2) = eqst b1 b2 && eqst c1 c2. Proof. by move=> *. Qed. Lemma eqst_prod : forall b1 c1 b2 c2, eqst (b1 ** c1) (b2 ** c2) = eqst b1 b2 && eqst c1 c2. Proof. by move=> *. Qed. Lemma eqst_sum : forall b1 c1 b2 c2, eqst (b1 +++ c1) (b2 +++ c2) = eqst b1 b2 && eqst c1 c2. Proof. by move=> *. Qed. Definition eqst_step := (pair eqst_arrow (pair eqst_prod eqst_sum)). Lemma eqstP : Equality.axiom eqst. Proof. intros a b; apply: (iffP idP). ... Qed. Canonical Structure st_eqMixin := EqMixin eqstP. Canonical Structure st_eqType := Eval hnf in (Equality.Pack st_eqMixin ST). (* Types *) Require Import List. Set Implicit Arguments. Fixpoint opt_nth (A:Type)(n:nat){struct n} : list A -> option A := fun l => match n,l with | O, (x::_) => Some x | S m, (_::l) => opt_nth m l | _,_ => None end. Lemma opt_nth_app : forall A g1 g2 (x:A), opt_nth (length g1)(g1++x::g2)=Some x. Proof. Lemma opt_nth_le : forall A (l1: list A) l2 n, n<(length l1) -> opt_nth n (l1++l2) = opt_nth n l1. Proof. Lemma opt_nth_gt : forall A (l1 : list A) l2 n, n>(length l1) -> opt_nth n (l1++l2) = opt_nth (n - length l1) l2. Proof. Lemma gt_opt_nth : forall A a (l:list A) n, opt_nth n l = Some a -> n < length l. Proof. Fixpoint infer (t : term) (G : list ST) {struct t} : option ST := match t with | Db j => opt_nth j G ... | Ifz t u1 u2 => match infer t G with | Some (Atomic Nat) => match infer u1 G, infer u2 G with | Some A, Some B => if A==B then Some A else None | _ , _ => None end | _ => None end ... | Fix A t => if infer t (A::G) is Some B then if A==B then Some B else None else None end. Lemma infer_clos : forall t G A, infer t G = Some A -> close t (length G). (* A faire vous même ou pas ... *) elim => //= [_ t1 ht1 t2 ht2|t ht u1 hu1 u2 hu2|B t ht|t ht u hu|i|t ht u hu|B t ht] G A. - case e1: (infer t1 G) => //=[[|||[|]]] //=; case e2: (infer t2 G) => //=[[|||[|]]]//= _. by apply/andP; split; eauto. - case e1: (infer t G) => //=[[|||[|]]] //=. case e2: (infer _ _ ) => //=; case e3: (infer _ _) => //=. by move => _; apply/andP; split; try (apply/andP; split); eauto. - case e: (infer _ _) => //= _; exact (ht _ _ e). - case e: (infer _ _) => //=[[C D|||]]//=; case eu: (infer _ _) => //= _. by apply /andP; split; eauto. - apply gt_opt_nth. - case et: (infer _ _) => //= eu; apply/andP; split; first by eauto. exact (hu _ _ eu). - rewrite /=; case e: (infer _ _) => //=[T]; case: (_ == _) => //= _. exact (ht _ _ e). Qed. (* Pour montrer que les termes typs dans le contexte vide sont clos, il faut généraliser l'hypothèse de récurrence. *) (* soit on pose la généralisation dans la preuve comme dans le script ci-dessous, soit on prouve d'abord quelque chose comme Lemma clos_infer : forall G u D A, infer u D = Some A -> infer u (D++G) = Some A. (la notation ++ est pour la concatenation; ici c'est formulé pour permettre la récurrence sur u *) Lemma clos_infer : forall u G A, infer u nil = Some A -> infer u G = Some A. Proof. move => u G A. have H : (forall D, infer u D = Some A -> infer u (D++G) = Some A); last exact (H (@nil ST)). move: A. elim: u => //= [_ t1 ht1 t2 ht2|t ht u1 hu1 u2 hu2|B t ht|t ht u hu|i|t ht u hu|B t ht] A D. - case e1: (infer t1 D) => [[|||[|]]|] //=. case e2: (infer t2 D) => [[|||[|]]|]//=. by rewrite (ht1 _ _ e1) (ht2 _ _ e2). - case e1: (infer t D) => //=[[|||[|]]] //=. case e2: (infer _ _ ) => [U1|//=]; case e3: (infer _ _) => [U2|//=]. case e12: (_ == _) => //=. move =>[UA]. case e4 : (infer _ _) => [[|||[|]]|]//=; try by rewrite (ht _ _ e1) in e4. by rewrite (hu1 _ _ e2) (hu2 _ _ e3) e12 UA. - rewrite app_comm_cons. case it: (infer _ _) => //= [T][<-]. by rewrite (ht T (B::D)). - case it: (infer _ _) => //= [[U T|||]]//=. case iu: (infer _ _) => [V|]//=. case UV : (_==_) => //=; move => [<-]. by rewrite (ht _ _ it)(hu _ _ iu) UV. - move => h; rewrite opt_nth_le. done. apply (gt_opt_nth _ _ h). - case it : (infer _ _) => [T|//=]. case iu : (infer _ _) => [U|//=][<-]. by rewrite (ht _ _ it)(hu _ _ iu). - case it : (infer _ _) => [T|//=]. case BT : (_==_) => //= <-. by rewrite (ht _ _ it) BT. Qed. Lemma subst_infer : forall t u D A, infer u nil = Some A -> infer t (D++A::nil) = infer (subst t (length D) u) D. Proof. .. Qed. Lemma beta_infer : forall t u, beta1 t u -> forall A, infer t nil = Some A -> infer u nil = Some A. Proof. move => t u; elim => [m n o |v B w |v w|v i T|v w|B v]/= A {t u}. ... Qed. Lemma val_int : forall t, value t -> forall G, infer t G = Some (Atomic Nat) -> {n:nat|t = Int n}. Proof. case => [o t u|n|t u v|T t|t u|j|t u|A t] h G tT; inversion h; first by exists n. .. Qed. Lemma val_fun : forall t, value t -> forall G A B, infer t G = Some (A-->B) -> {A : ST & {u : term | t = Fun A u}}. Proof. case => [o t u|n|t u v|T t|t u|j|t u|C t] h G A B tT; inversion h; first by move:tT =>//=. ... Qed. Lemma infer_value : forall t T, infer t nil = Some T -> (forall u, ~ congr beta1 t u) -> value t. Proof. elim => //= [o t ht u hu|t ht u hu v hv|t ht u hu|[|n]|t ht u hu|A t ht] T //=. (* A vous ou pas .. *) - case tT: (infer t nil) => [[|||[|]]|]//=; case uT: (infer u nil)=> [[|||[|]]|]//= _ ntu. have nt : (forall u, ~congr beta1 t u) by move => v tv; apply ntu with (Op o v u); apply congr_op_l. have nu : (forall v, ~congr beta1 u v) by move => v tv; apply ntu with (Op o t v); apply congr_op_r. move: (ht _ tT nt). case vt: t=>//= [n|] ; trivial; last by move: tT; rewrite vt /=; case: infer. move: (hu _ uT nu); case vu: u=>//=[m|]; trivial; last by move: uT; rewrite vu /=; case: infer. by elim (ntu (Int (op_op o n m))); rewrite vt vu; do 2 constructor. - case tT : (infer t nil) => [[|||[|]]|]//=. case uT : (infer u nil) => [U|]//=; case vT : (infer v nil) => [V|]//= _ ntuv. have nt : (forall u, ~congr beta1 t u) by move => w tw; apply ntuv with (Ifz w u v); apply congr_ifz_1. move: ntuv; move/(val_int _ (ht _ tT nt)): tT =>[[|it] ->] h. elim (h u); apply congr_base; constructor. elim (h v); apply congr_base; constructor. - case tT: (infer t nil) => [[A B|||]|]//= _ ntu. have nt : forall v, ~congr beta1 t v by move => v tv; elim (ntu (App v u)); apply congr_app_l. move: (val_fun _ (ht _ tT nt) _ tT) ntu => [U [w ->]] h. by elim (h (subst w 0 u)); apply congr_base; constructor. - move => _ h; elim (h (subst u 0 t)); apply congr_base; constructor. - move => _ h; elim (h (subst t 0 (Fix A t))); apply congr_base; constructor. Qed.