diff options
Diffstat (limited to 'samples/coq/Smallstep.v')
| -rwxr-xr-x | samples/coq/Smallstep.v | 701 |
1 files changed, 701 insertions, 0 deletions
diff --git a/samples/coq/Smallstep.v b/samples/coq/Smallstep.v new file mode 100755 index 0000000..b59bdd4 --- /dev/null +++ b/samples/coq/Smallstep.v @@ -0,0 +1,701 @@ +Require Export Imp. +Require Export Relations. + +Inductive tm : Type := + | tm_const : nat -> tm + | tm_plus : tm -> tm -> tm. + +Tactic Notation "tm_cases" tactic(first) ident(c) := + first; + [ Case_aux c "tm_const" | Case_aux c "tm_plus" ]. + +Module SimpleArith0. + +Fixpoint eval (t : tm) : nat := + match t with + | tm_const n => n + | tm_plus a1 a2 => eval a1 + eval a2 + end. + +End SimpleArith0. + +Module SimpleArith1. + +Reserved Notation " t '===>' n " (at level 50, left associativity). + +Inductive eval : tm -> nat -> Prop := + | E_Const : forall n, + tm_const n ===> n + | E_Plus : forall t1 t2 n1 n2, + t1 ===> n1 -> + t2 ===> n2 -> + tm_plus t1 t2 ===> plus n1 n2 + + where " t '===>' n " := (eval t n). + +End SimpleArith1. + +Reserved Notation " t '===>' t' " (at level 50, left associativity). + +Inductive eval : tm -> tm -> Prop := + | E_Const : forall n1, + tm_const n1 ===> tm_const n1 + | E_Plus : forall t1 n1 t2 n2, + t1 ===> tm_const n1 -> + t2 ===> tm_const n2 -> + tm_plus t1 t2 ===> tm_const (plus n1 n2) + where " t '===>' t' " := (eval t t'). + +Tactic Notation "eval_cases" tactic(first) ident(c) := + first; + [ Case_aux c "E_Const" | Case_aux c "E_Plus" ]. + +Module SimpleArith2. + +Reserved Notation " t '=>' t' " (at level 40). + +Inductive step : tm -> tm -> Prop := + | ST_PlusConstConst : forall n1 n2, + tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2) + | ST_Plus1 : forall t1 t1' t2, + t1 => t1' -> + tm_plus t1 t2 => tm_plus t1' t2 + | ST_Plus2 : forall n1 t2 t2', + t2 => t2' -> + tm_plus (tm_const n1) t2 => tm_plus (tm_const n1) t2' + + where " t '=>' t' " := (step t t'). + +Tactic Notation "step_cases" tactic(first) ident(c) := + first; + [ Case_aux c "ST_PlusConstConst" + | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ]. + +Example test_step_1 : + tm_plus + (tm_plus (tm_const 0) (tm_const 3)) + (tm_plus (tm_const 2) (tm_const 4)) + => + tm_plus + (tm_const (plus 0 3)) + (tm_plus (tm_const 2) (tm_const 4)). +Proof. + apply ST_Plus1. apply ST_PlusConstConst. Qed. + +Example test_step_2 : + tm_plus + (tm_const 0) + (tm_plus + (tm_const 2) + (tm_plus (tm_const 0) (tm_const 3))) + => + tm_plus + (tm_const 0) + (tm_plus + (tm_const 2) + (tm_const (plus 0 3))). +Proof. +apply ST_Plus2. +simpl. +apply ST_Plus2. +apply ST_PlusConstConst. +Qed. + +Theorem step_deterministic: + partial_function step. +Proof. + unfold partial_function. intros x y1 y2 Hy1 Hy2. + generalize dependent y2. + step_cases (induction Hy1) Case; intros y2 Hy2. + Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase. + SCase "ST_PlusConstConst". reflexivity. + SCase "ST_Plus1". inversion H2. + SCase "ST_Plus2". inversion H2. + Case "ST_Plus1". step_cases (inversion Hy2) SCase. + SCase "ST_PlusConstConst". rewrite <- H0 in Hy1. inversion Hy1. + SCase "ST_Plus1". + rewrite <- (IHHy1 t1'0). + reflexivity. assumption. + SCase "ST_Plus2". rewrite <- H in Hy1. inversion Hy1. + Case "ST_Plus2". step_cases (inversion Hy2) SCase. + SCase "ST_PlusConstConst". rewrite <- H1 in Hy1. inversion Hy1. + SCase "ST_Plus1". inversion H2. + SCase "ST_Plus2". + rewrite <- (IHHy1 t2'0). + reflexivity. assumption. Qed. + +End SimpleArith2. + +Inductive value : tm -> Prop := + v_const: forall n, value (tm_const n). + +Reserved Notation " t '=>' t' " (at level 40). + +Inductive step : tm -> tm -> Prop := + | ST_PlusConstConst : forall n1 n2, + tm_plus (tm_const n1) (tm_const n2) + => tm_const (plus n1 n2) + | ST_Plus1 : forall t1 t1' t2, + t1 => t1' -> + tm_plus t1 t2 => tm_plus t1' t2 + | ST_Plus2 : forall v1 t2 t2', + value v1 -> + t2 => t2' -> + tm_plus v1 t2 => tm_plus v1 t2' + + where " t '=>' t' " := (step t t'). + +Tactic Notation "step_cases" tactic(first) ident(c) := + first; + [ Case_aux c "ST_PlusConstConst" + | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ]. + +Theorem step_deterministic : + partial_function step. +Proof. +unfold partial_function. +intros x y1 y2 Hy1 Hy2. +generalize dependent y2. +step_cases (induction Hy1) Case; intros y2 Hy2. + step_cases (inversion Hy2) SCase. + reflexivity. + + inversion H2. + + inversion Hy2. + subst. + assumption. + + subst. + inversion H3. + + subst. + inversion H3. + + step_cases (inversion Hy2) SCase. + rewrite <- H0 in Hy1. + inversion Hy1. + + rewrite <- (IHHy1 t1'0). + reflexivity. + + assumption. + + rewrite <- H in Hy1. + rewrite <- H in H1. + subst. + inversion H1. + subst. + inversion Hy1. + + step_cases (inversion Hy2) SCase. + subst. + inversion Hy1. + + subst. + inversion H. + subst. + inversion H3. + + subst. + inversion H2. + subst. + rewrite <- (IHHy1 t2'0). + reflexivity. + + assumption. +Qed. + +Theorem strong_progress : forall t, + value t \/ (exists t', t => t'). +Proof. + tm_cases (induction t) Case. + Case "tm_const". left. apply v_const. + Case "tm_plus". right. inversion IHt1. + SCase "l". inversion IHt2. + SSCase "l". inversion H. inversion H0. + exists (tm_const (plus n n0)). + apply ST_PlusConstConst. + SSCase "r". inversion H0 as [t' H1]. + exists (tm_plus t1 t'). + apply ST_Plus2. apply H. apply H1. + SCase "r". inversion H as [t' H0]. + exists (tm_plus t' t2). + apply ST_Plus1. apply H0. Qed. + +Definition normal_form {X:Type} (R: relation X) (t: X) : Prop := + ~ (exists t', R t t'). + +Lemma value_is_nf: forall t, + value t -> normal_form step t. +Proof. + unfold normal_form. intros t H. inversion H. + intros contra. inversion contra. inversion H1. + Qed. + +Lemma nf_is_value: forall t, + normal_form step t -> value t. +Proof. + unfold normal_form. intros t H. + assert (G: value t \/ (exists t', t => t')). + SCase "Proof of assertion". apply strong_progress. + inversion G. + SCase "l". assumption. + SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed. + +Corollary nf_same_as_value : forall t, + normal_form step t <-> value t. +Proof. + split. apply nf_is_value. apply value_is_nf. +Qed. + +Module Temp1. + +Inductive value : tm -> Prop := +| v_const : forall n, value (tm_const n) +| v_funny : forall t1 n2, (* <---- *) + value (tm_plus t1 (tm_const n2)). + +Reserved Notation " t '=>' t' " (at level 40). + +Inductive step : tm -> tm -> Prop := + | ST_PlusConstConst : forall n1 n2, + tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2) + | ST_Plus1 : forall t1 t1' t2, + t1 => t1' -> + tm_plus t1 t2 => tm_plus t1' t2 + | ST_Plus2 : forall v1 t2 t2', + value v1 -> + t2 => t2' -> + tm_plus v1 t2 => tm_plus v1 t2' + + where " t '=>' t' " := (step t t'). + +Lemma value_not_same_as_normal_form: + exists t, value t /\ ~ normal_form step t. +Proof. +intros. +unfold normal_form. +exists (tm_plus (tm_plus (tm_const 1) (tm_const 2)) (tm_const 2)). +split. + apply v_funny. + + unfold not. + intros. + apply H. + exists (tm_plus (tm_const (1 + 2)) (tm_const 2)). + apply ST_Plus1. + apply ST_PlusConstConst. +Qed. + +End Temp1. + +Module Temp2. + +Inductive value : tm -> Prop := + | v_const : forall n, value (tm_const n). + +(*Reserved Notation " t '===>' t' " (at level 40).*) + +Inductive step : tm -> tm -> Prop := + | ST_Funny : forall n, (* <---- *) + tm_const n ===> tm_plus (tm_const n) (tm_const 0) + | ST_PlusConstConst : forall n1 n2, + tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2) + | ST_Plus1 : forall t1 t1' t2, + t1 ===> t1' -> + tm_plus t1 t2 ===> tm_plus t1' t2 + | ST_Plus2 : forall v1 t2 t2', + value v1 -> + t2 ===> t2' -> + tm_plus v1 t2 ===> tm_plus v1 t2' + + where " t '===>' t' " := (step t t'). + +Lemma value_not_same_as_normal_form : + exists t, value t /\ ~ normal_form step t. +Proof. +exists (tm_const 0). +split. + apply v_const. + + unfold normal_form. + unfold not. + intro H. + apply H. + exists (tm_plus (tm_const 0) (tm_const 0)). + apply ST_Funny. +Qed. + +End Temp2. + +Module Temp3. + +Inductive value : tm -> Prop := + | v_const : forall n, value (tm_const n). + +(*Reserved Notation " t '===>' t' " (at level 40).*) + +Inductive step : tm -> tm -> Prop := + | ST_PlusConstConst : forall n1 n2, + tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2) + | ST_Plus1 : forall t1 t1' t2, + t1 ===> t1' -> + tm_plus t1 t2 ===> tm_plus t1' t2 + + where " t '===>' t' " := (step t t'). + +Lemma value_not_same_as_normal_form: + exists t, ~ value t /\ normal_form step t. +Proof. +exists (tm_plus (tm_const 1) (tm_plus (tm_const 0) (tm_const 0))). +split. + intros H. + inversion H. + + unfold normal_form. + intros H. + inversion H. + inversion H0. + inversion H4. +Qed. + +End Temp3. + +Module Temp4. +Inductive tm : Type := + | tm_true : tm + | tm_false : tm + | tm_if : tm -> tm -> tm -> tm. + +Inductive value : tm -> Prop := + | v_true : value tm_true + | v_false : value tm_false. + +Inductive step : tm -> tm -> Prop := + | ST_IfTrue : forall t1 t2, + tm_if tm_true t1 t2 ===> t1 + | ST_IfFalse : forall t1 t2, + tm_if tm_false t1 t2 ===> t2 + | ST_If : forall t1 t1' t2 t3, + t1 ===> t1' -> + tm_if t1 t2 t3 ===> tm_if t1' t2 t3 + + where " t '===>' t' " := (step t t'). + +Example bool_step_prop3 : + tm_if + (tm_if tm_true tm_true tm_true) + (tm_if tm_true tm_true tm_true) + tm_false + ===> + tm_if + tm_true + (tm_if tm_true tm_true tm_true) + tm_false. +Proof. +apply ST_If. +apply ST_IfTrue. +Qed. + +Theorem strong_progress: forall t, + value t \/ (exists t', t ===> t'). +Proof. +induction t. + left. + constructor. + + left. + constructor. + + right. + inversion IHt1. + inversion H. + exists t2. + apply ST_IfTrue. + + exists t3. + apply ST_IfFalse. + + inversion H. + exists (tm_if x t2 t3). + apply ST_If. + assumption. +Qed. + +Theorem step_deterministic : + partial_function step. +Proof. +unfold partial_function. +intros x y1 y2 Hy1 Hy2. +generalize dependent y2. +induction Hy1. + intros. + inversion Hy2. + reflexivity. + + subst. + inversion H3. + + intros. + inversion Hy2. + reflexivity. + + inversion H3. + + intros. + inversion Hy2. + subst. + inversion Hy1. + + subst. + inversion Hy1. + + subst. + apply IHHy1 in H3. + subst. + reflexivity. +Qed. + +Module Temp5. + + +Inductive step : tm -> tm -> Prop := + | ST_IfTrue : forall t1 t2, + tm_if tm_true t1 t2 ===> t1 + | ST_IfFalse : forall t1 t2, + tm_if tm_false t1 t2 ===> t2 + | ST_If : forall t1 t1' t2 t3, + t1 ===> t1' -> + tm_if t1 t2 t3 ===> tm_if t1' t2 t3 + | ST_ShortCut : forall v t, + value v -> + tm_if t v v ===> v + + where " t '===>' t' " := (step t t'). + +Definition bool_step_prop4 := + tm_if + (tm_if tm_true tm_true tm_true) + tm_false + tm_false + ===> + tm_false. + +Example bool_step_prop4_holds : + bool_step_prop4. +Proof. + unfold bool_step_prop4. + apply ST_ShortCut. + constructor. +Qed. + +Theorem strong_progress: forall t, + value t \/ (exists t', t ===> t'). +Proof. + induction t. + left. + constructor. + + left. + constructor. + + inversion IHt1. + right. + inversion H. + exists t2. + constructor. + + exists t3. + constructor. + + right. + inversion H. + exists (tm_if x t2 t3). + apply ST_If. + assumption. +Qed. + +End Temp5. +End Temp4. + +Definition stepmany := refl_step_closure step. + +Notation " t '===>*' t' " := (stepmany t t') (at level 40). + +Lemma test_stepmany_1: + tm_plus + (tm_plus (tm_const 0) (tm_const 3)) + (tm_plus (tm_const 2) (tm_const 4)) + ===>* + tm_const (plus (plus 0 3) (plus 2 4)). +Proof. + eapply rsc_step. apply ST_Plus1. apply ST_PlusConstConst. + eapply rsc_step. apply ST_Plus2. apply v_const. + apply ST_PlusConstConst. + eapply rsc_step. apply ST_PlusConstConst. + apply rsc_refl. Qed. + +Lemma test_stepmany_2: + tm_const 3 ===>* tm_const 3. +Proof. + eapply rsc_refl. +Qed. + +Lemma test_stepmany_3: + tm_plus (tm_const 0) (tm_const 3) + ===>* + tm_plus (tm_const 0) (tm_const 3). +Proof. + eapply rsc_refl. +Qed. + +Lemma test_stepmany_4: + tm_plus + (tm_const 0) + (tm_plus + (tm_const 2) + (tm_plus (tm_const 0) (tm_const 3))) + ===>* + tm_plus + (tm_const 0) + (tm_const (plus 2 (plus 0 3))). +Proof. +eapply rsc_step. + apply ST_Plus2. + apply v_const. + + apply ST_Plus2. + apply v_const. + + apply ST_PlusConstConst. + + eapply rsc_step. + apply ST_Plus2. + apply v_const. + + apply ST_PlusConstConst. + + eapply rsc_refl. +Qed. + +Definition step_normal_form := normal_form step. + +Definition normal_form_of (t t' : tm) := + (t ===>* t' /\ step_normal_form t'). + + (* +Theorem normal_forms_unique: + partial_function normal_form_of. +Proof. + unfold partial_function. unfold normal_form_of. intros x y1 y2 P1 P2. + destruct P1 as [P11 P12]. destruct P2 as [P21 P22]. + generalize dependent y2. + + unfold step_normal_form in P12. + unfold step_normal_form. + unfold normal_form. + unfold normal_form in P12. + induction x. + intros. + unfold stepmany. + inversion P11. + subst. + inversion P21. + subst. + reflexivity. + + subst. + inversion P21. + reflexivity. + + subst. + inversion H1. + + inversion H. + *) + +Definition normalizing {X:Type} (R:relation X) := + forall t, exists t', + (refl_step_closure R) t t' /\ normal_form R t'. + +Lemma stepmany_congr_1 : forall t1 t1' t2, + t1 ===>* t1' -> + tm_plus t1 t2 ===>* tm_plus t1' t2. +Proof. +intros t1 t1' t2 H. +rsc_cases (induction H) Case. + apply rsc_refl. + + apply rsc_step with (tm_plus y t2). + apply ST_Plus1. + apply H. + + apply IHrefl_step_closure. +Qed. + +Lemma stepmany_congr2 : forall t1 t2 t2', + value t1 -> + t2 ===>* t2' -> + tm_plus t1 t2 ===>* tm_plus t1 t2'. +Proof. +intros t1 t2 t2'. +intros H1. +intros H2. +induction H2. + apply rsc_refl. + + apply rsc_step with (tm_plus t1 y). + apply ST_Plus2. + assumption. + + assumption. + + assumption. +Qed. + +Theorem step_normalizing : + normalizing step. +Proof. + unfold normalizing. + tm_cases (induction t) Case. + Case "tm_const". + exists (tm_const n). + split. + SCase "l". apply rsc_refl. + SCase "r". + (* We can use rewrite with "iff" statements, not + just equalities: *) + rewrite nf_same_as_value. apply v_const. + Case "tm_plus". + destruct IHt1 as [t1' H1]. destruct IHt2 as [t2' H2]. + destruct H1 as [H11 H12]. destruct H2 as [H21 H22]. + rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22. + inversion H12 as [n1]. inversion H22 as [n2]. + rewrite <- H in H11. + rewrite <- H0 in H21. + exists (tm_const (plus n1 n2)). + split. + SCase "l". + apply rsc_trans with (tm_plus (tm_const n1) t2). + apply stepmany_congr_1. apply H11. + apply rsc_trans with + (tm_plus (tm_const n1) (tm_const n2)). + apply stepmany_congr2. apply v_const. apply H21. + apply rsc_R. apply ST_PlusConstConst. + SCase "r". + rewrite nf_same_as_value. apply v_const. Qed. + + Lemma eval__value : forall t1 t2, + eval t1 t2 -> + value t2. + Proof. + intros t1 t2 HE. + eval_cases (inversion HE) Case; apply v_const. Qed. + + + (* +Theorem eval__stepmany: forall t v, + eval t v -> t ===>* v. +Proof. +*) |