Add LoadPath "/users/profs/info/werner/COQ/". Require Arith. Require Import ssreflect. Require Import ssrnat. Require Import ssrbool. Require Import eqtype. Add LoadPath ".". Require Import my_omega. (* Types : definition et égalité *) Inductive atomic : Type := | Nat | Bool. Inductive ST : Type := | STArr : ST -> ST -> ST | STProd : ST -> ST -> ST | STSum : ST -> ST -> ST | Atomic of atomic. Notation "A --> B" := (STArr A B) (at level 55, right associativity). Notation "A ** B" := (STProd A B) (at level 55, right associativity). Notation "A +++ B" := (STSum A B) (at level 45, right associativity). (* Les notations sont utilisables dans les motifs *) Definition pat_test_bidon (T : ST) : bool := match T with | A --> B => true | _ => false end. (* termes *) Inductive op :Type := OpPlus | OpMult | OpMinus. Inductive term : Type := | Op : op -> term -> term ->term | Int :> nat -> term | Ifz : term -> term -> term -> term | Fun : ST -> term -> term | App : term -> term -> term | Db of nat | Let : term -> term -> term | Fix : ST -> term -> term. Fixpoint subst (t:term)(i:nat)(u:term){struct t} := match t with | Op o t1 t2 => Op o (subst t1 i u)(subst t2 i u) | Int n => t | Ifz t1 t2 t3 => Ifz (subst t1 i u)(subst t2 i u)(subst t3 i u) | Fun A t => Fun A (subst t (S i) u) | App t1 t2 => App (subst t1 i u)(subst t2 i u) | Db j => if i==j then u else t | Let a t => Let (subst a i u)(subst t (S i) u) | Fix A a => Fix A (subst a (S i) u) end. Fixpoint close (t:term)(i:nat) {struct t} : bool := match t with | Op o t1 t2 => close t1 i && close t2 i | Int n => true | Ifz t1 t2 t3 => close t1 i && (close t2 i && close t3 i) | Fun A t => close t (S i) | App t1 t2 => close t1 i && close t2 i | Db j => j < i | Let a t => (close a i) && (close t (S i)) | Fix _ a => (close a (S i)) end. Lemma close_mon : forall t i, close t i -> close t (S i). Proof. elim => /=; try auto; first move => o; try (move => t1 ht1 t2 ht2 i; move/andP=>[h1 h2]//=; apply /andP; split; auto). move=> t1 ht1 t2 ht2 t3 ht3 i; move/andP=>[h1]; move/andP=>[h2 h3]; apply/andP. by split; try auto; apply/andP; split; auto. Qed. Lemma close_close : forall t n, close t 0 -> close t n. Proof. by move => t; elim => //= n hn ct; apply close_mon; auto. Qed. Hint Resolve close_mon close_close. Lemma subst_close : forall t u i, close u i -> close t (S i) -> close (subst t i u) i. elim => //=; first move => o; try (move => t1 ht1 t2 ht2 u i cu; move/andP=>[h1 h2]//=; apply /andP; split; auto). - move => t1 ht1 t2 ht2 t3 ht3 u i cu; move/andP=>[h1]; move/andP=>[h3 h2]//=. by do 2 (apply /andP; split; auto). - by move=> _ t ht u i cu ct; apply ht=>//; apply close_mon. - move=> n u i cu; case e: (i==n)=> /=; first done. Search (_=(_<_)). by move: (neq_ltn i n); rewrite e; myo. by auto. Qed. Set Implicit Arguments. (* small steps semantics *) Definition op_op (o:op) : nat -> nat -> nat := match o with | OpPlus => addn | OpMinus => minus | OpMult => mult end. Inductive beta1 : term -> term -> Prop := | Op_red : forall n m o, beta1 (Op o (Int n)(Int m))(Int (op_op o n m)) | Beta_red : forall t A u, beta1 (App (Fun A t) u)(subst t 0 u) | Ifz_0_red : forall t u, beta1 (Ifz (Int 0) t u) t | Ifz_1_red : forall t u n, beta1 (Ifz (Int (S n)) t u) u | Let_red : forall t u, beta1 (Let t u)(subst u 0 t) | Fix_red : forall A u, beta1 (Fix A u)(subst u 0 (Fix A u)). Inductive congr (R:term->term->Prop) : term -> term -> Prop := | congr_base : forall t u, R t u -> congr R t u | congr_op_l : forall t t1 u o, congr R t t1 -> congr R (Op o t u)(Op o t1 u) | congr_op_r : forall t u u1 o, congr R u u1 -> congr R (Op o t u)(Op o t u1) | congr_app_l : forall t t1 u, congr R t t1 -> congr R (App t u)(App t1 u) | congr_app_r : forall t u u1, congr R u u1 -> congr R (App t u)(App t u1) (* | congr_fun : forall A t t1, congr R t t1 -> congr R (Fun A t)(Fun A t1) *) | congr_ifz_1 : forall t t1 u v, congr R t t1 -> congr R (Ifz t u v)(Ifz t1 u v) | congr_ifz_2 : forall t u u1 v, congr R u u1 -> congr R (Ifz t u v)(Ifz t u1 v) | congr_ifz_3 : forall t u v v1, congr R v v1 -> congr R (Ifz t u v)(Ifz t u v1) | congr_let_l : forall t t1 u, congr R t t1 -> congr R (Let t u)(Let t1 u) (* | congr_let_lr : forall t u u1, congr R u u1 -> congr R (Let t u)(Let t u1) | cong_letrec : forall A t t1, congr R t t1 -> congr R (Fix A t)(Fix A t1) *) . Definition interp_op (o:op) := match o with | OpPlus => plus | OpMult => mult | OpMinus => minus end. Definition progressed := (term*bool)%type. (* éxécute une étape de réduction si possible *) Fixpoint bstep (t:term) : progressed := match t with | Op o (Int n) (Int m) => (Int (interp_op o n m),true) | Op o (Int n) t => let (t',p) := (bstep t) in (Op o (Int n) t', p) | Op o t1 t2 => let (t',p) := (bstep t1) in (Op o t' t2, p) | (Ifz (Int 0) t _) => (t,true) | (Ifz (Int (S _)) _ t) => (t,true) | (Ifz c t1 t2) => let (c',p) := (bstep c) in (Ifz c' t1 t2,p) | App (Fun _ t) u => (subst t 0 u,true) | App t u => let (t',p) := bstep t in (App t' u , p ) | Let e t => (subst t 0 e , true) | Fix a u => (subst u 0 t , true) | _ => (t,false) end. Fixpoint iter (n:nat) (t:term) { struct n } := match n with | 0 => t | S n => match bstep t with | (t',true) => iter n t' | _ => t end end. (* Essayez en executant de petits programmes *) (* Eval compute in (iter 100 .....). *) Definition exec (n:nat) (t:term) := let aux := fix aux (n:nat) (t:term) { struct n } := match n with | 0 => bstep t | S n => let R := aux n in match R t with | (t',true) => let (t'',_) := R t' in (t'',true) | u => u end end in fst (aux n t). (* Pour ceux qui se débrouillent bien: vous pouvez commencer des preuves de correction *) (* sur le modele suivant *) Lemma step_correct_false : forall t,forall t', bstep t = (t',false) -> t=t'. Proof. elim => //=. - move=> o t1 ht1 t2 ht2 t'. case et1 : t1 ht1 => [|n||||||]; try (case: (bstep _) => //= t b e ee;move: (ee)=> [<- _]; auto; rewrite (e t); auto; move: ee => [_ ->] //). clear t1 et1. move => _. case et2 : t2 ht2 => [|m||||||]; case: (bstep _) => //= t b e ee; try (move: (ee)=> [<- _]; auto; rewrite (e t); auto; move: ee => [_ ->] //). - by move=> n t' h; inversion h. - move => t ht t0 ht0 t1 _; case et : t ht => [|n||||||]; try (case: (bstep _) => //= u b e v ee;move: (ee)=> [<- _]; rewrite (e u); auto; move: ee => [_ ->] //). by clear et; case: n. - by move => T t _ t' h; inversion h. - move => t ht u hu. move => t'. by case: t ht => [o v1 v2|m|v v0 v1|T t|v1 v2|i|v1 v2|V v]; (case eb: (bstep _) => [w b]; move => e ee; rewrite (e w); inversion ee). - by move => n t' e; inversion e. Qed. Lemma step_correct_true : forall t t', bstep t = (t',true) -> congr beta1 t t'. Proof. elim => //= [o t1 ht1 t2 ht2|||| ]. (* ...... *) (* Assez difficile *) Admitted. (* Analyse des résultats de calculs : valeurs *) Definition value (t:term) : bool := match t with | Int _ => true | Fun _ _ => true | _ => false end. Lemma value_norm : forall t u, value t -> ~congr beta1 t u. Proof. elim =>//=; first by move => n u _ h; inversion_clear h; inversion H. move => A t _ u _ h; inversion_clear h; inversion H. Qed. Lemma beta_clos : forall t u, beta1 t u -> close t 0 -> close u 0. move => t u; elim {t u}=> //= [t _ u|bt|bt|bt|bt]. - by move/andP=>[*]; apply subst_close. - by move => u; move/andP=>[*]. - by move => u _; move/andP=>[*]. - by move => u; move/andP=>[*]; apply subst_close. - by move => u cu; apply subst_close. Qed. (* Semantique à grands pas *) Inductive sem_op : term -> term -> Prop := | op_val_int : forall n, sem_op (Int n)(Int n) | op_val_fun : forall A t, sem_op (Fun A t)(Fun A t) | op_val_op : forall t vt u vu o, sem_op t (Int vt) -> sem_op u (Int vu) -> sem_op (Op o t u)(Int (op_op o vt vu)) | op_app : forall t A vt u vu w, sem_op t (Fun A vt) -> sem_op u vu -> sem_op (subst vt O vu) w -> sem_op (App t u) w | op_let : forall t u vu vt, sem_op u vu -> sem_op (subst t 0 vu) vt -> sem_op (Let u t) vt | op_srec : forall A t vt, sem_op (subst t O (Fix A t)) vt -> sem_op (Fix A t) vt | op_ifz0 : forall t u v vu, sem_op t (Int 0) -> sem_op u vu -> sem_op (Ifz t u v) vu | op_ifz1 : forall t u v vv i, sem_op t (Int (S i)) -> sem_op v vv -> sem_op (Ifz t u v) vv. Lemma big_value : forall t vt, sem_op t vt -> value vt. Proof. move=> t vt; elim =>//=. Qed. Inductive congrt (R : term -> term -> Prop)(t : term) : term -> Prop := | congrt_refl : congrt R t t | congr_step : forall t2 t3, congrt R t t2 -> congr R t2 t3 -> congrt R t t3. Lemma congr_trans : forall R t1 t2 t3, congrt R t1 t2 -> congrt R t2 t3 -> congrt R t1 t3. Proof. move => R t1 t2 t3 t12; elim => //=. by move => t4 *; apply congr_step with t4. Qed. Lemma congrt_op_l : forall R t t' u o, congrt R t t' -> congrt R (Op o t u)(Op o t' u). move=>R t t' u o; elim; first by constructor. move=> t1 t2 rtt1 ro rt12. apply congr_step with (Op o t1 u); first done. by apply congr_op_l. Qed. Lemma congrt_op_r : forall R t t' u o, congrt R t t' -> congrt R (Op o u t)(Op o u t'). move=>R t t' u o; elim; first by constructor. move=> t1 t2 rtt1 ro rt12. apply congr_step with (Op o u t1); first done. by apply congr_op_r. Qed. Lemma congrt_app_l : forall R t t' u, congrt R t t' -> congrt R (App t u)(App t' u). move=>R t t' u; elim; first by constructor. move=> t1 t2 rtt1 rta12 tr12. apply congr_step with (App t1 u); first done. by apply congr_app_l. Qed. Lemma congrt_app_r : forall R t t' u, congrt R t t' -> congrt R (App u t)(App u t'). move=>R t t' u; elim; first by constructor. move=> t1 t2 rtt1 rta12 tr12. apply congr_step with (App u t1); first done. by apply congr_app_r. Qed. Lemma congrt_ifz1 : forall R t t1 u v, congrt R t t1 -> congrt R (Ifz t u v)(Ifz t1 u v). move => R t t1 u v; elim; first by constructor. move=> t2 t3 ct2 ci c23; apply congr_step with (Ifz t2 u v); first done. by apply congr_ifz_1. Qed. Lemma congrt_ifz2 : forall R t u u1 v, congrt R u u1 -> congrt R (Ifz t u v)(Ifz t u1 v). move => R t u u1 v; elim; first by constructor. move=> u2 u3 ct2 ci c23; apply congr_step with (Ifz t u2 v); first done. by apply congr_ifz_2. Qed. Lemma congrt_ifz3 : forall R t u v v1, congrt R v v1 -> congrt R (Ifz t u v)(Ifz t u v1). move => R t u v v1; elim; first by constructor. move=> v2 v3 ct2 ci c23; apply congr_step with (Ifz t u v2); first done. by apply congr_ifz_3. Qed. Lemma congrt_let : forall R t t1 u, congrt R t t1 -> congrt R (Let t u)(Let t1 u). move => T t t1 u; elim; first by constructor. move => t2 t3 ctt2 cl ct23; apply congr_step with (Let t2 u); first done. by apply congr_let_l. Qed. Lemma big_small : forall t vt, sem_op t vt -> congrt beta1 t vt. Proof. move=> t vt; elim => {t vt} [||t vt u vu o tv rtv tu rtu |t A vt u vu w rtv ruv cu rtw cw cs||||]; try (constructor; constructor). - apply congr_step with (Op o vt vu); last by apply congr_base; constructor. apply congr_trans with (Op o vt u). by apply congrt_op_l. by apply congrt_op_r. - apply congr_trans with (App (Fun A vt) u). by apply congrt_app_l. apply congr_trans with (App (Fun A vt) vu); first by apply congrt_app_r. apply congr_trans with (subst vt 0 vu); last done. apply congr_step with (App (Fun A vt) vu); first by constructor. apply congr_base; apply Beta_red. - move => t u vu vt *. apply congr_trans with (Let vu t); first by apply congrt_let. apply congr_trans with (subst t 0 vu); last done. apply congr_step with (Let vu t); first by constructor. by apply congr_base; apply Let_red. - move => A t vt *; apply congr_trans with (subst t 0 (Fix A t)); last done. apply congr_step with (Fix A t); first by constructor. by apply congr_base; exact (Fix_red _ _). -move => t u v vu *; apply congr_trans with (Ifz 0 u v); first by apply congrt_ifz1. apply congr_trans with u; last done. apply congr_step with (Ifz 0 u v); first by constructor. apply congr_base; apply Ifz_0_red. -move => t u v vu i *; apply congr_trans with (Ifz (S i) u v); first by apply congrt_ifz1. apply congr_trans with v; last done. apply congr_step with (Ifz (S i) u v); first by constructor. apply congr_base; apply Ifz_1_red. Qed.