diff --git a/BigStep.v b/BigStep.v new file mode 100644 index 0000000..20687f1 --- /dev/null +++ b/BigStep.v @@ -0,0 +1,646 @@ +From Coq Require Import + Strings.String + Bool.Bool + Init.Datatypes + Lists.List + Logic.FunctionalExtensionality (* for equality of substitutions *) + Ensembles + Psatz + Classes.RelationClasses. + +From BigStepSymbEx Require Import +Limits +Expr +Maps +Syntax . + +Import While. +Open Scope com_scope. + +Fixpoint loop_fuel__C (fuel: nat) (f: Valuation -> option Valuation) (b: Bexpr) (V: Valuation): option Valuation := + match fuel with + | 0 => None + | S n => if Beval V b + then option_bind (f V) (loop_fuel__C n f b) + else Some V + end. + +Lemma loop_mono: forall i j f b V, + i <= j -> loop_fuel__C i f b V <<= loop_fuel__C j f b V. +Proof. + induction i; intros; simpl. + - constructor. + - destruct j. + + inversion H. + + simpl; destruct (Beval V b). + * apply option_bind_mono. + -- apply lessdef_refl. + -- intro. apply IHi. lia. + * constructor. +Qed. + +(** Concrete semantics *) +Definition loop__C (f: Valuation -> option Valuation) (b: Bexpr) (V: Valuation) : option Valuation := + limit (fun n => loop_fuel__C n f b V) (fun i j => loop_mono i j f b V). + +Fixpoint denot_fun (p: Stmt) (V: Valuation): option Valuation := + match p with + | <{skip}> => Some V + | <{x := e}> => Some (x !-> Aeval V e ; V) + | <{p1 ; p2}> => option_bind (denot_fun p1 V) (denot_fun p2) + | <{if b {p1} {p2}}> => if Beval V b then (denot_fun p1 V) else (denot_fun p2 V) + | <{while b {p}}> => loop__C (denot_fun p) b V + end. + +(* Characterizing the concrete denotation *) +Lemma loop_charact__C: forall f b V, exists i, forall j, i <= j -> loop_fuel__C j f b V = loop__C f b V. +Proof. intros. apply limit_charact. Qed. + +Lemma loop_unique__C: forall f b V i lim, + (forall j, i <= j -> loop_fuel__C j f b V = lim) -> + loop__C f b V = lim. +Proof. + intros. destruct (loop_charact__C f b V) as [i' LIM]. + set (j := Nat.max i i'). + rewrite <- (H j). rewrite (LIM j). reflexivity. + all: lia. +Qed. + +Lemma denot_seq: forall p1 p2 V, + denot_fun <{p1 ; p2}> V = option_bind (denot_fun p1 V) (denot_fun p2). +Proof. reflexivity. Qed. + +Lemma denot_loop: forall f b V, + loop__C f b V = if Beval V b then option_bind (f V) (loop__C f b) else Some V. +Proof. + intros. + destruct (f V) eqn:H. + - destruct (loop_charact__C f b v) as [i LIM]. + apply loop_unique__C with (i := (S i)). intros. + destruct j; [lia|]. + simpl. destruct (Beval V b); + try reflexivity. + rewrite H; cbn. apply LIM. lia. + - destruct (loop_charact__C f b V) as [i LIM]. + apply loop_unique__C with (i := (S i)). intros. + destruct j; [lia|]. + simpl. destruct (Beval V b); + [rewrite H|]; reflexivity. +Qed. + +Lemma denot_loop_seq: forall p b V, + denot_fun <{while b {p}}> V = denot_fun <{if b {p ; while b {p}} {skip}}> V. +Proof. + intros. simpl. rewrite denot_loop. + destruct (Beval V b); reflexivity. +Qed. + +Lemma loop_false: forall f b V, Beval V b = false -> loop__C f b V = Some V. +Proof. intros. rewrite denot_loop. rewrite H. reflexivity. Qed. + +(** Symbolic Semantics *) + +Section EnsembleHelpers. + Variable X: Type. + Variable A B C: Ensemble X. + + Lemma intersect_full: Intersection X (Full_set _) A = A. + Proof. + intros. apply Extensionality_Ensembles. split; intros x H. + - destruct H; assumption. + - split; [constructor | assumption]. + Qed. + + Lemma intersect_comm: Intersection _ A B = Intersection _ B A. + Proof. + intros. apply Extensionality_Ensembles. split; intros x H; + destruct H; split; assumption. + Qed. + + Lemma intersect_assoc: Intersection _ A (Intersection _ B C) = Intersection _ (Intersection _ A B) C. + Proof. + intros. apply Extensionality_Ensembles. split; intros x H; repeat split; + try (destruct H; destruct H0; assumption); + destruct H; destruct H; assumption. + Qed. +End EnsembleHelpers. + + +Definition Branch: Type := (Valuation -> Valuation) * (Ensemble Valuation). + +Definition denot_sub (phi: sub): Valuation -> Valuation := fun V => Comp V phi. + +Lemma denot_id_sub: denot_sub id_sub = fun V => V. +Proof. unfold denot_sub. extensionality V. rewrite comp_id. reflexivity. Qed. + +Definition inverse_image {X: Type} (F: X -> X) (B: Ensemble X): Ensemble X := fun x => B (F x). + +(* characterizing inverse images *) +Lemma inverse_id {X:Type}: forall (A: Ensemble X), inverse_image (fun x => x) A = A. +Proof. intros. apply Extensionality_Ensembles. split; intros V H; assumption. Qed. + +Lemma inverse_full {X:Type}: forall F, inverse_image F (Full_set _) = Full_set X. +Proof. intros. apply Extensionality_Ensembles. split; intros V _; constructor. Qed. + +Lemma inverse_empty {X:Type}: forall F, inverse_image F (Empty_set _) = Empty_set X. +Proof. intros. apply Extensionality_Ensembles. split; intros V H; inversion H. Qed. + +Lemma inverse_complement {X:Type}: forall F B, + inverse_image F (Complement _ B) = Complement X (inverse_image F B). +Proof. + intros. apply Extensionality_Ensembles. split; intros V H. + - intro contra. apply H. apply contra. + - apply H. +Qed. + +Lemma inverse_intersection {X:Type}: forall F B1 B2, + inverse_image F (Intersection _ B1 B2) = Intersection X (inverse_image F B1) (inverse_image F B2). +Proof. + intros. apply Extensionality_Ensembles. split; intros V H. + - inversion H; subst. split; assumption. + - destruct H. split; assumption. +Qed. + +Lemma inverse_inverse {X:Type}: forall F F' (B: Ensemble X), + inverse_image F (inverse_image F' B) = inverse_image (fun x => F' (F x)) B. +Proof. + intros. apply Extensionality_Ensembles. split; intros V H. + - apply H. + - apply H. +Qed. + +Definition denot__B (b: Bexpr): Ensemble Valuation := fun V => Beval V b = true. + +(* Characterizing denot__B *) +Lemma denotB_true: forall V b, In _ (denot__B b) V <-> Beval V b = true. +Proof. split; intros; apply H. Qed. + +Lemma denotB_false: forall V b, In _ (Complement _ (denot__B b)) V <-> Beval V b = false. +Proof. + split; intros. + - apply (not_true_is_false _ H). + - unfold Complement, In, denot__B. intro. rewrite H in H0. discriminate. +Qed. + +Lemma denotB_top: denot__B (BTrue) = Full_set _. +Proof. + apply Extensionality_Ensembles. split; intros V _. + - apply Full_intro. + - unfold denot__B, In. reflexivity. +Qed. + +Lemma denotB_bot: denot__B BFalse = Empty_set _. +Proof. apply Extensionality_Ensembles. split; intros V H; inversion H. Qed. + +Lemma denotB_neg: forall b, denot__B <{~ b}> = Complement _ (denot__B b). +Proof. + intros. apply Extensionality_Ensembles. split; intros V H. + - intro contra. inversion H. inversion contra. + rewrite negb_true_iff in H1. rewrite H1 in H2. discriminate. + - unfold denot__B, Ensembles.In. simpl. rewrite negb_true_iff. + apply not_true_is_false in H. apply H. +Qed. + +Lemma denotB_and: forall b1 b2, + denot__B <{b1 && b2}> = Intersection _ (denot__B b1) (denot__B b2). +Proof. + intros. apply Extensionality_Ensembles. split; intros V H. + - inversion H. apply andb_true_iff in H1. destruct H1. + split; assumption. + - destruct H. + unfold denot__B, Ensembles.In. simpl. rewrite andb_true_iff. + split; assumption. +Qed. + +(* Equation (1) *) +Lemma denot_sub_sound: forall sigma V e, + Aeval (denot_sub sigma V) e = Aeval V (Aapply sigma e). +Proof. unfold denot_sub. intros. apply comp_sub. Qed. + +(* Equation (2) *) +Lemma inverse_denotB: forall s b, + denot__B (Bapply s b) = inverse_image (denot_sub s) (denot__B b). +Proof. + intros. induction b. + - simpl. rewrite denotB_top. rewrite inverse_full. reflexivity. + - simpl. rewrite denotB_bot. rewrite inverse_empty. reflexivity. + - simpl. rewrite 2 denotB_neg. rewrite IHb. rewrite inverse_complement. reflexivity. + - simpl. rewrite 2 denotB_and. rewrite IHb1, IHb2. rewrite inverse_intersection. reflexivity. + - apply Extensionality_Ensembles. split; intros V H. + + inversion H. rewrite <- 2 denot_sub_sound in H1. + unfold inverse_image, In. unfold denot_sub. apply H1. + + inversion H. + unfold denot__B, Ensembles.In. simpl. unfold denot_sub in H1. + rewrite <- 2 comp_sub. apply H1. +Qed. + +Fixpoint n_fold {X: Type} (n: nat) (f: X -> X): X -> X := + match n with + | 0 => fun x => x + | S n => fun x => f (n_fold n f x) + end. + +Lemma n_fold_inversion {X:Type}: forall n f (x: X), f (n_fold n f x) = n_fold (S n) f x. +Proof. reflexivity. Qed. + +Lemma n_fold_step {X:Type}: forall n f (x y: X), n_fold (S n) f x = y -> exists z, n_fold n f x = z /\ f z = y. +Proof. + induction n; intros; simpl in *. + - exists x. split; [reflexivity | apply H]. + - exists (f (n_fold n f x)). split; [reflexivity | apply H]. +Qed. + +Lemma n_fold_construct {X:Type}: forall n f (x y z: X), + n_fold n f x = y -> f y = z -> n_fold (S n) f x = z. +Proof. + induction n; intros; simpl in *. + - rewrite H. apply H0. + - rewrite (IHn f x (n_fold n f x) y). + + assumption. + + reflexivity. + + assumption. +Qed. + +Definition loop_helper (body: Ensemble Branch) (b: Bexpr) (p: Stmt): Ensemble Branch -> Ensemble Branch := + fun big_F => fun X => exists F B Fp Bp, + In _ big_F (F, B) + /\ In _ body (Fp, Bp) + /\ fst X = (fun V => F (Fp V)) + /\ snd X = Intersection _ (denot__B b) (Intersection _ Bp (inverse_image Fp B)). + +Lemma loop_helper_step: forall n body b p F B X0, + In _ (n_fold (S n) (loop_helper body b p) X0) (F, B) -> + exists F' B', In _ (n_fold n (loop_helper body b p) X0) (F', B') + /\ loop_helper body b p (Singleton _ (F', B')) (F, B) +. +Proof. + intros. + destruct (n_fold_step n (loop_helper body b p) X0 (n_fold (S n) (loop_helper body b p) X0)) + as [Y [H0 H1]]; [reflexivity|]. + destruct H as [F' [B' [Fp [Bp [Hbody [Hloop [tmp0 tmp1]]]]]]]. + simpl in tmp0, tmp1; subst. + exists F'. exists B'. repeat split. + - apply Hbody. + - exists F'. exists B'. exists Fp. exists Bp. + repeat split. apply Hloop. +Qed. + +Inductive Union_Fam {X I} (Fs: I -> Ensemble X): Ensemble X := + | Fam_intro: forall {i x}, In _ (Fs i) x -> In _ (Union_Fam Fs) x. + +Fixpoint denot__S (p: Stmt): Ensemble Branch := match p with + | <{skip}> => Singleton _ (fun V => V, Full_set _) + | <{x := e}> => Singleton _ (fun V => (x !-> Aeval V e ; V), Full_set _) + | <{p ; q}> => + fun X => exists Fp Fq Bp Bq, + In _ (denot__S p) (Fp, Bp) + /\ In _ (denot__S q) (Fq, Bq) + /\ (fst X = fun V => Fq (Fp V)) + /\ snd X = Intersection _ Bp (inverse_image Fp Bq) + | <{if b {p} {q}}> => + fun X => + (exists F B, + In _ (denot__S p) (F, B) + /\ fst X = F + /\ snd X = Intersection _ B (denot__B b)) + \/ + (exists F B, + In _ (denot__S q) (F, B) + /\ fst X = F + /\ snd X = Intersection _ B (Complement _ (denot__B b))) + | <{while b {p}}> => + Union_Fam (fun m => n_fold m (loop_helper (denot__S p) b p) (Singleton _ (fun V => V, Complement _ (denot__B b)))) + end. + +Lemma denot_seq__S: forall p1 p2 F1 F2 B1 B2, + In _ (denot__S p1) (F1, B1) -> + In _ (denot__S p2) (F2, B2) -> + In _ (denot__S <{p1 ; p2}>) (fun V => F2 (F1 V), Intersection _ B1 (inverse_image F1 B2)). +Proof. + intros. + exists F1. exists F2. exists B1. exists B2. + repeat split; assumption. +Qed. + +Lemma denot_if__S: forall b p1 p2 F1 F2 B1 B2, + In _ (denot__S p1) (F1, B1) -> + In _ (denot__S p2) (F2, B2) -> + In _ (denot__S <{if b {p1} {p2}}>) (F1, Intersection _ B1 (denot__B b)) + /\ In _ (denot__S <{if b {p1} {p2}}>) (F2, Intersection _ B2 (Complement _ (denot__B b))). +Proof. + intros. split. + - left. exists F1. exists B1. repeat split. assumption. + - right. exists F2. exists B2. repeat split. assumption. +Qed. + +Lemma denot_while0__S: forall b p, + In _ (denot__S <{while b {p}}>) (fun V => V, Complement _ (denot__B b)). +Proof. intros. exists 0. constructor. Qed. + +Lemma denot_while1__S: forall b p F B, + In _ (denot__S p) (F, B) -> + In _ (denot__S <{while b {p}}>) (F, + Intersection _ (denot__B b) (Intersection _ B (inverse_image F (Complement _ (denot__B b))))). +Proof. + intros. exists 1. + simpl. + exists (fun V => V). exists (Complement _ (denot__B b)). + exists F. exists B. repeat split. + apply H. +Qed. + +Lemma denot_while__S: forall b p F B Floop Bloop, + In _ (denot__S p) (F, B) -> + In _ (denot__S <{while b {p}}>) (Floop, Bloop) -> + In _ (denot__S <{while b {p}}>) + (fun V => Floop (F V), Intersection _ (denot__B b) (Intersection _ B (inverse_image F Bloop))). +Proof. + intros. inversion H0; subst. + apply Fam_intro with (i := S i). + exists Floop. exists Bloop. exists F. exists B. + repeat split; + assumption. +Qed. + +Lemma loop_complete: forall i p b V V', + loop_fuel__C (S i) (denot_fun p) b V = Some V' -> + (forall Vbody Vbody', + denot_fun p Vbody = Some Vbody' -> + exists F B, + In _ (denot__S p) (F, B) + /\ F Vbody = Vbody' + /\ In _ B Vbody) -> + exists F B, + In _ (Union_Fam (fun m => n_fold m (loop_helper (denot__S p) b p) (Singleton _ (fun V => V, Complement _ (denot__B b))))) (F, B) + /\ F V = V' + /\ In _ B V +. +Proof. + induction i; intros. + - simpl in H. destruct (Beval V b) eqn:Hbeval, (denot_fun p V); cbn in H; + inversion H. + + exists (fun V => V). exists (Complement _ (denot__B b)). repeat split. + * apply Fam_intro with (i := 0). simpl. + constructor. + * rewrite denotB_false. rewrite <- H2. apply Hbeval. + + exists (fun V => V). exists (Complement _ (denot__B b)). repeat split. + * apply Fam_intro with (i := 0). simpl. + constructor. + * rewrite denotB_false. rewrite <- H2. apply Hbeval. + - simpl in H. destruct (Beval V b) eqn:Hbeval; destruct (denot_fun p V) eqn:Hbody; cbn in *. + + destruct (IHi _ _ _ _ H H0) as [F [B [Hin [HF HB]]]]. + inversion Hin as [i' [? ?]]; subst. + destruct (H0 V v Hbody) as [F' [B' [Hin' [HF' HB']]]]. + exists (fun V => F (F' V)). eexists. + repeat split. + * apply Fam_intro with (i := S i'). + exists F. exists B. exists F'. exists B'. + repeat split. + -- apply H1. + -- apply Hin'. + * rewrite HF'. reflexivity. + * repeat split. + -- rewrite denotB_true. apply Hbeval. + -- apply HB'. + -- unfold inverse_image, In. + rewrite HF'. + apply HB. + + inversion H. + + inversion H; subst. + specialize (IHi p b V' V'). + rewrite Hbeval in IHi. + destruct (IHi H H0) as [F [B [Hin [HF HB]]]]. + inversion Hin as [i' [? ?]]; subst. + exists F. exists B. repeat split. + * apply Hin. + * apply HF. + * apply HB. + + inversion H; subst. + specialize (IHi p b V' V'). + rewrite Hbeval in IHi. + destruct (IHi H H0) as [F [B [Hin [HF HB]]]]. + inversion Hin as [i' [? ?]]; subst. + exists F. exists B. repeat split. + * apply Hin. + * apply HF. + * apply HB. +Qed. + +Lemma complete: forall p V V', + denot_fun p V = Some V' -> + exists F B, + In _ (denot__S p) (F, B) + /\ F V = V' + /\ In _ B V. +Proof. + induction p; intros. + (* skip *) + - exists (fun V => V). + exists (Full_set _). + simpl in *. repeat split; + inversion H; reflexivity. + (* assign *) + - exists (fun V => (x !-> Aeval V e ; V)). + exists (Full_set _). + simpl in *. repeat split; + inversion H; reflexivity. + (* sequence *) + - inversion H; subst. + destruct (option_inversion H1) as [V1 [? ?]]. + destruct (IHp1 _ _ H0) as [F1 [B1 [Hbranch1 [Hresult1 Hpart1]]]]. + destruct (IHp2 _ _ H2) as [F2 [B2 [Hbranch2 [Hresult2 Hpart2]]]]. + exists (fun V => F2 (F1 V)). + exists (Intersection _ B1 (inverse_image F1 B2)). + simpl in *. split; try split. + + exists F1. exists F2. exists B1. exists B2. repeat split; + assumption. + + rewrite Hresult1. apply Hresult2. + + split. + * apply Hpart1. + * unfold inverse_image, In. + rewrite Hresult1. apply Hpart2. + (* if... *) + - inversion H; subst. destruct (Beval V b) eqn:Hbeval. + (*... true*) + + destruct (IHp1 _ _ H1) as [F1 [B1 [Hbranch [Hresult Hpart]]]]. + exists F1. exists (Intersection _ B1 (denot__B b)). split; try split. + * left. exists F1. exists B1. repeat split. + apply Hbranch. + * apply Hresult. + * split. + -- apply Hpart. + -- rewrite denotB_true. apply Hbeval. + (*... false*) + + destruct (IHp2 _ _ H1) as [F2 [B2 [Hbranch [Hresult Hpart]]]]. + exists F2. exists (Intersection _ B2 (Complement _ (denot__B b))). split; try split. + * right. exists F2. exists B2. repeat split. + apply Hbranch. + * apply Hresult. + * split. + -- apply Hpart. + -- rewrite denotB_false. apply Hbeval. + (* while *) + - inversion H; subst; destruct (Beval V b) eqn:Hbeval. + (* looping *) + + rewrite denot_loop in H1. rewrite Hbeval in H1. + destruct (option_inversion H1) as [? [? ?]]. + destruct (IHp _ _ H0) as [F [B [Hbody [HF HB]]]]. + destruct (loop_charact__C (denot_fun p) b x) as [i LIM]. + rewrite <- LIM with (j := S i) in H2; [|lia]. + destruct (loop_complete _ _ _ _ _ H2 IHp) as [F' [B' [Hhelp [HF' HB']]]]. + exists (fun V => F' (F V)). exists (Intersection _ (denot__B b) (Intersection _ B (inverse_image F B'))). + split; try split. + * apply denot_while__S. + -- apply Hbody. + -- simpl. apply Hhelp. + * rewrite HF. apply HF'. + * split. + -- rewrite denotB_true. apply Hbeval. + -- split. + ++ apply HB. + ++ unfold inverse_image, In. rewrite HF. apply HB'. + (* end of loop *) + + rewrite denot_loop in H1. + rewrite Hbeval in H1. + exists (fun V => V). exists (Complement _ (denot__B b)). repeat split. + * apply Fam_intro with (i := 0). + simpl. constructor. + * inversion H1. reflexivity. + * rewrite denotB_false. apply Hbeval. +Qed. + +Lemma loop_correct: forall i p b F B V0, + In _ (n_fold i (loop_helper (denot__S p) b p) + (Singleton _ (fun V => V, Complement Valuation (denot__B b)))) + (F, B) -> + (forall F' B' V, + In _ (denot__S p) (F', B') -> + In _ B' V -> + exists V', F' V = V' + /\ denot_fun p V = Some V') -> + In _ B V0 -> + exists V, + F V0 = V + /\ loop__C (denot_fun p) b V0 = Some V. +Proof. + induction i; intros. + - simpl in H. inversion H; subst. + exists V0. split. + + reflexivity. + + apply loop_false. rewrite <- denotB_false. apply H1. + - destruct (loop_helper_step _ _ _ _ _ _ _ H) as [F' [B' [Hsofar H2]]]. + inversion H2 as [F0 [B0 [Fp [Bp [? [? [? ?]]]]]]]. + simpl in H5, H6. inversion H3. subst. + inversion H1; inversion H6; subst. + destruct (H0 Fp Bp V0 H4 H8) as [V' [? ?]]. + destruct (IHi _ _ _ _ (Fp V0) Hsofar H0 H9) as [V'' [? ?]]. + exists V''. split. + + apply H11. + + rewrite denot_loop. rewrite H5. rewrite H10; cbn. + rewrite <- H7. apply H12. +Qed. + +Lemma correct: forall p F B V, + In _ (denot__S p) (F, B) -> + In _ B V -> + exists V', F V = V' /\ denot_fun p V = Some V'. +Proof. + induction p; intros. + - inversion H; subst. + exists V. split; reflexivity. + - inversion H; subst. + exists (x !-> Aeval V e; V). split; reflexivity. + - destruct H as [F1 [F2 [B1 [B2 [H1 [H2 [HF HB]]]]]]]. + exists (F2 (F1 V)). split. + + simpl in HF. rewrite HF. reflexivity. + + simpl in *. + rewrite HB in H0. inversion H0; subst. + destruct (IHp1 F1 B1 V H1 H) as [V1 [? HV1]]. rewrite HV1. + destruct (IHp2 F2 B2 (F1 V) H2 H3) as [V2 [? HV2]]. + simpl. + rewrite <- H4. rewrite HV2. rewrite H5. + reflexivity. + - simpl. destruct H; destruct (Beval V b) eqn:Hcond. + (* condition true, left branch*) + + destruct H as [F1 [B1 [H1 [HF HB]]]]. + simpl in HB. rewrite HB in H0. inversion H0; subst. + destruct (IHp1 F B1 V H1 H) as [V1 [HF1 HV1]]. + exists V1. split; assumption. + (* condition false, left branch => contradiction *) + + destruct H as [F1 [B1 [H1 [HF HB]]]]. + simpl in HB. rewrite HB in H0. inversion H0; subst. + unfold denot__B, In in H2. rewrite H2 in Hcond. + discriminate. + (* condition true, right branch => contradiction*) + + destruct H as [F2 [B2 [H2 [HF HB]]]]. + simpl in HB. rewrite HB in H0. inversion H0; subst. + unfold denot__B, In, Complement in H1. + exfalso. apply H1. apply Hcond. + (* condition false, right branch *) + + destruct H as [F2 [B2 [H2 [HF HB]]]]. + simpl in HB. rewrite HB in H0. inversion H0; subst. + destruct (IHp2 F B2 V H2 H) as [V2 [HF2 HV2]]. + exists V2. split; assumption. + - inversion H; subst; cbn. + apply (loop_correct _ _ _ _ _ V H1 IHp H0). +Qed. + +(** definition of big step symbolic as partial function *) +Section PartialSymbEx. + (* Lemma 1 *) + Hypothesis pairwise_disjoint_preconditions: forall p F B F' B', + In _ (denot__S p) (F, B) -> + In _ (denot__S p) (F', B') -> + Inhabited _ (Intersection _ B B') -> + (F, B) = (F', B'). + + (* Definition 1 *) + Inductive big_step_partial (p: Stmt): Valuation -> Valuation -> Prop := + | big_step_intro: forall F B v, + In _ (denot__S p) (F, B) -> + In _ B v -> + big_step_partial p v (F v). + + Definition partial_function {X: Type} (R: X -> X -> Prop) := + forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2. + + Lemma complement_disjoint {X: Type}: forall (A: Ensemble X), Disjoint _ A (Complement _ A). + Proof. + intros. constructor. intros x contra. + inversion contra; subst. + apply H0. apply H. + Qed. + + Lemma disjoint_not_inhabited {X: Type}: forall (A B: Ensemble X), + Disjoint _ A B -> + Inhabited _ (Intersection _ A B) -> + False. + Proof. + intros. inversion H. inversion H0. + apply (H1 x). apply H2. + Qed. + + Theorem big_step_is_partial_function: forall p, partial_function (big_step_partial p). + Proof. + unfold partial_function. intros. + inversion H; subst. inversion H0; subst. + assert (Inhabited _ (Intersection _ B B0)) by + (apply (Inhabited_intro _ _ x); split; assumption). + specialize (pairwise_disjoint_preconditions _ _ _ _ _ H1 H3 H5); intros. + inversion pairwise_disjoint_preconditions. + reflexivity. + Qed. + + (* Theorem 1 *) + Theorem concrete_symbolic_correspondence: forall p v v', + denot_fun p v = Some v' <-> big_step_partial p v v'. + Proof. + split; intros. + - apply complete in H. destruct H as (F & B & Hin & HF & HB). + rewrite <- HF. + apply (big_step_intro p F B v Hin HB). + - inversion H; subst. + destruct (correct _ _ _ _ H0 H1) as (v' & HF & Heval). + subst. apply Heval. + Qed. +End PartialSymbEx. diff --git a/BigStepExamples.v b/BigStepExamples.v new file mode 100644 index 0000000..bcbf335 --- /dev/null +++ b/BigStepExamples.v @@ -0,0 +1,107 @@ +From Coq Require Import + Strings.String + Bool.Bool + Psatz + ZArith + Ensembles. + +From BigStepSymbEx Require Import + BigStep + Expr + Maps + Syntax +. +Import While. +Open Scope com_scope. + +(** concrete *) +Definition option_apply {A B: Type}: option (A -> B) -> A -> option B := + fun f a => match f with + | None => None + | Some f => Some (f a) + end. + +Compute option_apply (denot_fun + <{if X <= 10 {X := X + 1; + if X <= 5 {Y := X + X} + { skip }} + { Y := 42 }}> + (_ !-> 11)) Y. + +(* gives a very ugly result *) +(* Compute option_apply (denot_fun *) +(* <{while X <= 10 {X := X + 1; *) +(* if X <= 5 {Y := X + X} *) +(* { skip }} }> *) +(* (_ !-> 0)) X. *) + +(** symbolic *) +Example branch_example: Stmt := <{ + if X <= 0 + {if 1 <= 0 {X := 42} {X := 0}} + {if 1 <= 0 {X := 42} {X := 1}} + }>. + + +Example branch_1: denot__S branch_example (fun V => (X !-> 42 ; V), Empty_set _). +Proof. + left. exists (fun V => (X !-> 42 ; V)). eexists. repeat split. + - left. exists (fun V => (X !-> 42 ; V)). eexists. repeat split. + - simpl. apply Extensionality_Ensembles. split. + + intros V H. inversion H. + + intros V H. inversion H; subst; inversion H0; inversion H3. +Qed. + +Example branch_2: denot__S branch_example (fun V => (X !-> 42 ; V), Empty_set _). +Proof. + right. eexists. eexists. repeat split. + - left. eexists. eexists. repeat split. + - simpl. apply Extensionality_Ensembles. split. + + intros V H. inversion H. + + intros V H. inversion H; subst; inversion H0; inversion H3. +Qed. + +Example branch_3: denot__S branch_example (fun V => (X !-> 0 ; V), fun V => V X = 0). +Proof. + left. eexists. eexists. repeat split. + - right. eexists. eexists. repeat split. + - apply Extensionality_Ensembles. split; intros V H. + + inversion H. split. + * split. + -- apply Full_intro. + -- intro. rewrite H1 in H0. inversion H0. + * rewrite H1. unfold denot__B, In. simpl. rewrite H1. reflexivity. + + inversion H. inversion H1. apply leb_complete in H4. inversion H4. reflexivity. +Qed. + +Lemma leb_correct_neg: forall n m, n <=? m <> true -> ~ (n <= m). +Proof. intros n m H contra. apply H. apply leb_correct. apply contra. Qed. + +Example branch_4: denot__S branch_example (fun V => (X !-> 1 ; V), fun V => V X > 0). +Proof. + right. eexists. eexists. repeat split. + - right. eexists. eexists. repeat split. + - apply Extensionality_Ensembles. split; intros V H. + + inversion H; repeat split; intro; inversion H0. + * rewrite <- H1 in H3. discriminate. + * inversion H2. + * inversion H2. rewrite <- H0 in H5. discriminate. + + inversion H. unfold In. simpl. + unfold Complement, In, denot__B in H1. simpl in H1. + apply leb_correct_neg in H1. apply not_le in H1. + assumption. +Qed. + +Example loop_example: Stmt := + <{ while X <= 10 {X := X + 1} }>. + +Example loop_0: denot__S loop_example (fun V => V, fun V => V X > 10). +Proof. apply Fam_intro with (i := 0). cbn. + assert (Complement _ (denot__B <{ X <= 10 }>) = fun V => V X > 10). + { apply Extensionality_Ensembles. repeat split; intros V H. + - unfold Complement, In, denot__B in H. simpl in H. apply leb_correct_neg in H. + apply not_le in H. apply H. + - intro H'. unfold In, denot__B in *. simpl in *. apply leb_complete in H'. lia. + } + rewrite H. constructor. +Qed. diff --git a/Correspondence.v b/Correspondence.v new file mode 100644 index 0000000..5f1b257 --- /dev/null +++ b/Correspondence.v @@ -0,0 +1,446 @@ +From Coq Require Import + String Bool Datatypes Relations Program.Equality Classes.RelationClasses + Relations.Operators_Properties + Logic.FunctionalExtensionality (* for equality of substitutions *) + Ensembles + Lists.List +. +Import ListNotations. + +From BigStepSymbEx Require Import Expr + Syntax + Maps + BigStep + SmallStep +. +Import While. + +Open Scope com_scope. +Open Scope string_scope. +Open Scope list_scope. + +(** Substitutions *) +(* Definition 2 *) +Fixpoint acc_subst (t: trace__S) (sig: sub): sub := + match t with + | [] => sig + | Asgn x e :: t => acc_subst t (x !-> Aapply sig e; sig) + | _ :: t => acc_subst t sig + end. + +Lemma acc_subst_asgn_last: forall t sig x e, + acc_subst (t ++ [Asgn x e]) sig = (x !-> Aapply (acc_subst t sig) e ; acc_subst t sig). +Proof. + induction t; intros. + - reflexivity. + - destruct a; simpl. + + rewrite IHt. reflexivity. + + apply IHt. +Qed. + +Lemma acc_subst_cond_last: forall t sig b, + acc_subst (t ++ [Cond b]) sig = acc_subst t sig. +Proof. + induction t; intros. + - reflexivity. + - destruct a; simpl; apply IHt. +Qed. + +Lemma acc_subst_concat: forall s t sig, + acc_subst (s ++ t) sig = acc_subst t (acc_subst s sig). +Proof. + induction s; intros. + - reflexivity. + - destruct a; simpl. + + rewrite IHs. reflexivity. + + apply IHs. +Qed. + +Lemma asgn_acc_subst': forall sig x e V y, + denot_sub (acc_subst [Asgn x e] id_sub) (denot_sub sig V) y = denot_sub (x !-> Aapply sig e ; sig) V y. +Proof. + intros. unfold denot_sub; simpl. + rewrite 2 asgn_sound. rewrite comp_id. reflexivity. +Qed. + +Lemma asgn_acc_subst: forall sig x e, + (fun V => denot_sub (acc_subst [Asgn x e] id_sub) (denot_sub sig V)) + = denot_sub (x !-> Aapply sig e ; sig). +Proof. intros. extensionality V. extensionality y. apply asgn_acc_subst'. Qed. + +Lemma acc_subst_comp: forall t sig, + denot_sub (acc_subst t sig) = fun V => denot_sub (acc_subst t id_sub) (denot_sub sig V). +Proof. + induction t using rev_ind; intros. + - simpl. rewrite denot_id_sub. reflexivity. + - destruct x. + + rewrite 2 acc_subst_asgn_last. + rewrite <- 2 asgn_acc_subst. + rewrite IHt. reflexivity. + + rewrite 2 acc_subst_cond_last. + apply IHt. +Qed. + +(* Lemma 2 *) +Lemma acc_subst_concat_comp: forall s t, + denot_sub (acc_subst (s ++ t) id_sub) = fun V => denot_sub (acc_subst t id_sub) (denot_sub (acc_subst s id_sub) V). +Proof. + intros. + rewrite acc_subst_concat. + rewrite acc_subst_comp. + reflexivity. +Qed. + +(** Path Conditions *) +(* Definition 3 *) +Fixpoint acc_pc (t: trace__S) (sig: sub): Bexpr := + match t with + | [] => BTrue + | Asgn x e :: t => acc_pc t (x !-> Aapply sig e; sig) + | Cond b :: t => BAnd (Bapply sig b) (acc_pc t sig) + end. + +Lemma acc_pc_asgn_last: forall t sig x e, + acc_pc (t ++ [Asgn x e]) sig = acc_pc t sig. +Proof. + induction t; intros. + - reflexivity. + - destruct a; simpl. + + apply IHt. + + rewrite IHt. reflexivity. +Qed. + +Lemma acc_pc_cond_last: forall t sig b, + denot__B (acc_pc (t ++ [Cond b]) sig) = denot__B (BAnd (acc_pc t sig) (Bapply (acc_subst t sig) b)). +Proof. + induction t; intros. + - simpl. rewrite 2 denotB_and. + apply intersect_comm. + - destruct a; simpl. + + rewrite IHt. reflexivity. + + rewrite denotB_and, IHt. + rewrite 3 denotB_and, intersect_assoc. + reflexivity. +Qed. + +Lemma intersect_full' {X:Type}: forall A, Intersection X A (Full_set _) = A. +Proof. + intros. apply Extensionality_Ensembles. split; intros x H. + - destruct H; assumption. + - split; [assumption | constructor]. +Qed. + +Lemma denot_acc_pc_cond: forall b, denot__B (acc_pc [Cond b] id_sub) = denot__B b. +Proof. intros. simpl. rewrite Bapply_id, denotB_and, denotB_top, intersect_full'. auto. Qed. + +Lemma concat_pc: forall s t sig, + denot__B (acc_pc (s ++ t) sig) = denot__B (BAnd (acc_pc s sig) (acc_pc t (acc_subst s sig))). +Proof. + induction s; intros. + - simpl. rewrite denotB_and, denotB_top, intersect_full. + reflexivity. + - destruct a; simpl. + + rewrite IHs, denotB_and. + reflexivity. + + rewrite 3 denotB_and, IHs, denotB_and. + rewrite <- intersect_assoc. + reflexivity. +Qed. + +Lemma backwards_comp: forall t sig, + denot__B (acc_pc t sig) = inverse_image (denot_sub sig) (denot__B (acc_pc t id_sub)). +Proof. + induction t using rev_ind; intros. + - simpl. rewrite denotB_top, + inverse_full. + reflexivity. + - destruct x; simpl. + + rewrite 2 acc_pc_asgn_last. apply IHt. + + rewrite 2 acc_pc_cond_last. + rewrite <- inverse_denotB; simpl. + rewrite 2 denotB_and. + rewrite 2 (inverse_denotB sig). + rewrite (inverse_denotB (acc_subst t sig)). + rewrite (inverse_denotB (acc_subst t id_sub)). + rewrite inverse_inverse. + rewrite <- IHt. + rewrite acc_subst_comp. + reflexivity. +Qed. + +(* Lemma 3 *) +Lemma pc_concat_intersect: forall s t, + denot__B (acc_pc (s ++ t) id_sub) = + Intersection _ (denot__B (acc_pc s id_sub)) (inverse_image (denot_sub (acc_subst s id_sub)) (denot__B (acc_pc t id_sub))). +Proof. + intros. + rewrite concat_pc. + rewrite denotB_and. + rewrite <- backwards_comp. + reflexivity. +Qed. + +(** Theorem 11: big-small step correspondence *) +Definition PHI (t: trace__S): Branch := + (denot_sub (acc_subst t id_sub), denot__B (acc_pc t id_sub)). + +Definition feasible (t: trace__S): Prop := + Inhabited _ (denot__B (acc_pc t id_sub)). + +Lemma empty_feasible: feasible []. +Proof. unfold feasible. simpl. rewrite denotB_top. + apply Inhabited_intro with (x := (_ !-> 0)). + constructor. +Qed. + +Lemma feasible_app: forall s t, + feasible (s ++ t) -> feasible s /\ feasible t. +Proof. + destruct s; intros. + - split. + + apply empty_feasible. + + rewrite app_nil_l in H; assumption. + - unfold feasible; destruct t; simpl; inversion H; subst; split. + + rewrite pc_concat_intersect in H0. simpl in H0. + destruct H0. apply Inhabited_intro with (x := x0); assumption. + + rewrite pc_concat_intersect in H0. simpl in H0. + destruct H0. set (foo := (denot_sub (acc_subst s (x !-> Aapply id_sub e; id_sub)))). + apply Inhabited_intro with (x := foo x0); assumption. + + rewrite pc_concat_intersect in H0; simpl in H0. + destruct H0. apply Inhabited_intro with (x := x); assumption. + + rewrite pc_concat_intersect in H0; simpl in H0. destruct H0. + apply Inhabited_intro with (x := (denot_sub (acc_subst s id_sub)) x); assumption. +Qed. + +Lemma small_to_big_loop': forall b p t, + canonical <{while b {p}}> t -> + feasible t -> + (forall t', + canonical p t' -> feasible t' -> Ensembles.In Branch (denot__S p) (denot_sub (acc_subst t' id_sub), denot__B (acc_pc t' id_sub))) -> + Ensembles.In Branch (denot__S <{ while b {p} }>) (denot_sub (acc_subst t id_sub), denot__B (acc_pc t id_sub)). +Proof. + intros. destruct (canonical_loop _ _ _ H) as (m & ts & -> & ?). + induction m. + - simpl. rewrite denot_id_sub, denotB_and, denotB_neg, denotB_top, Bapply_id, intersect_full'. + exists 0. constructor. + - (* setup for denot_while__S *) + replace (build_loop_trace b (S m) ts) + with ([Cond b] ++ ts m ++ build_loop_trace b m ts) by auto. + rewrite 3 acc_subst_concat_comp. + replace (acc_subst [Cond <{ ~ b }>] id_sub) with id_sub by auto. + rewrite <- app_assoc. + rewrite pc_concat_intersect. + rewrite <- app_assoc. + rewrite pc_concat_intersect. + replace (acc_subst [Cond b] id_sub) with id_sub by auto. + rewrite denot_id_sub. + replace (denot__B (acc_pc [Cond b] id_sub)) with (denot__B b) + by (symmetry; apply denot_acc_pc_cond). + + (* this is entirely unnecessary, but cleans goal up to show how denot_while__S applies *) + set (F := denot_sub (acc_subst (ts m) id_sub)). + set (Floop := denot_sub (acc_subst (build_loop_trace b m ts) id_sub)). + set (B := denot__B (acc_pc (ts m) id_sub)). + set (Bloop := denot__B (acc_pc (build_loop_trace b m ts ++ [Cond <{ ~ b }>]) id_sub)). + + apply denot_while__S. + + apply H1. + * apply H2. auto. + * replace (build_loop_trace b (S m) ts ++ [Cond <{ ~ b }>]) + with ([Cond b] ++ (ts m) ++ (build_loop_trace b m ts) ++ [Cond <{~ b}>]) in H0 + by (simpl; rewrite <- app_assoc; auto). + destruct (feasible_app _ _ H0) as (_ & ?). + destruct (feasible_app _ _ H3) as (? & _). + assumption. + + subst Floop. subst Bloop. + replace (acc_subst (build_loop_trace b m ts ++ [Cond <{ ~ b }>]) id_sub) + with (acc_subst (build_loop_trace b m ts) id_sub) in IHm + by (rewrite acc_subst_cond_last; auto). + apply IHm. + * replace (build_loop_trace b (S m) ts ++ [Cond <{ ~ b }>]) + with ([Cond b] ++ (ts m) ++ (build_loop_trace b m ts) ++ [Cond <{~ b}>]) in H0 + by (simpl; rewrite <- app_assoc; auto). + destruct (feasible_app _ _ H0) as (_ & ?). + destruct (feasible_app _ _ H3) as (_ & ?). + assumption. + * apply loop_canonical. intros. apply H2. constructor. apply H3. + * intros. apply H2. transitivity m. assumption. apply PeanoNat.Nat.lt_succ_diag_r. +Qed. + +Theorem small_to_big: forall p t, + canonical p t -> + feasible t -> + Ensembles.In _ (denot__S p) (PHI t). +Proof. + unfold PHI. induction p; intros. + - rewrite canonical_skip in H; subst; simpl. + rewrite denot_id_sub, denotB_top. + constructor. + - rewrite canonical_asgn in H; subst; simpl. + unfold denot_sub. + assert (F_ext: (fun V => Comp V (x !-> Aapply id_sub e; id_sub)) + = (fun V => (x !-> Aeval V e; V))) + by (extensionality V; rewrite asgn_sound, comp_id; reflexivity). + rewrite F_ext, denotB_top. + constructor. + - destruct (sequence_concat _ _ _ H) as (t1 & t2 & Happ & Ht1 & Ht2); + subst; simpl. + destruct (feasible_app _ _ H0). + specialize (IHp1 _ Ht1 H1). + specialize (IHp2 _ Ht2 H2). + exists (denot_sub (acc_subst t1 id_sub)). + exists (denot_sub (acc_subst t2 id_sub)). + exists (denot__B (acc_pc t1 id_sub)). + exists (denot__B (acc_pc t2 id_sub)). + repeat split; try assumption. + + simpl. apply acc_subst_concat_comp. + + simpl. rewrite concat_pc, denotB_and. + rewrite <- backwards_comp. + reflexivity. + - rewrite canonical_if in H. + destruct H as [t' H]. destruct H. + + destruct H as [Happ Hcanon]. + rewrite Happ in H0. + destruct (feasible_app _ _ H0). + specialize (IHp1 _ Hcanon H1). + subst. left. + exists (denot_sub (acc_subst t' id_sub)). + exists (denot__B (acc_pc t' id_sub)). + repeat split; try assumption. + * simpl. rewrite denotB_and, Bapply_id. + apply intersect_comm. + + destruct H as [Happ Hcanon]. + rewrite Happ in H0. + destruct (feasible_app _ _ H0). + specialize (IHp2 _ Hcanon H1). + subst. right. + exists (denot_sub (acc_subst t' id_sub)). + exists (denot__B (acc_pc t' id_sub)). + repeat split; try assumption. + * simpl. + rewrite denotB_and, denotB_neg, Bapply_id. + apply intersect_comm. + - apply small_to_big_loop'; assumption. +Qed. + +Theorem big_to_small: forall p F B, + Ensembles.In _ (denot__S p) (F, B) -> + Inhabited _ B -> + exists t, canonical p t /\ PHI t = (F, B). +Proof. + induction p; intros. + - exists []. split. + + constructor. + + inversion H; subst. + unfold PHI; simpl. + rewrite denot_id_sub, denotB_top. + reflexivity. + - exists [Asgn x e]. split. + + apply canonical_asgn. reflexivity. + + inversion H; subst. + unfold PHI; simpl. + rewrite denotB_top. + unfold denot_sub. + replace (fun V : Valuation => Comp V (x !-> Aapply id_sub e; id_sub)) + with (fun V : total_map => x !-> Aeval V e; V) + by (extensionality V; rewrite asgn_sound, comp_id; reflexivity). + reflexivity. + - destruct H as (F1 & F2 & B1 & B2 & ? & ? & ? & ?). + simpl in H2, H3. subst. + inversion H0. destruct H2. + assert (InB1: Inhabited _ B1) by (apply Inhabited_intro with (x := x); assumption). + assert (InB2: Inhabited _ B2) by (apply Inhabited_intro with (x := F1 x); assumption). + destruct (IHp1 _ _ H InB1) as (t1 & Hcanon & HPHI). + destruct (IHp2 _ _ H1 InB2) as (t2 & Hcanon' & HPHI'). + inversion HPHI; subst. inversion HPHI'; subst. + exists (t1 ++ t2). split. + + apply concat_sequence; assumption. + + unfold PHI. + rewrite acc_subst_concat_comp. + rewrite pc_concat_intersect. + reflexivity. + - destruct H as [Htrue | Hfalse]. + + destruct Htrue as (F' & B' & Inp1 & ? & ?). + simpl in H, H1; subst. + inversion H0. destruct H. + assert (InB': Inhabited _ B') by (apply Inhabited_intro with (x := x); assumption). + destruct (IHp1 _ _ Inp1 InB') as (t1 & Hcanon & HPhi). + exists (Cond b :: t1). split. + * apply clos_rt1n_rtn1. econstructor. + -- apply red_cond_true. + -- simpl. + replace (Cond b :: t1) with ([Cond b] ++ t1) by reflexivity. + apply clos_rtn1_rt1n. apply canonical_extends; assumption. + * inversion HPhi; subst. + unfold PHI; simpl. + rewrite denotB_and, Bapply_id, intersect_comm. + reflexivity. + + destruct Hfalse as (F' & B' & Inp2 & ? & ?). + simpl in H, H1; subst. + inversion H0. destruct H. + assert (InB': Inhabited _ B') by (apply Inhabited_intro with (x := x); assumption). + destruct (IHp2 _ _ Inp2 InB') as (t2 & Hcanon & HPhi). + exists (Cond <{~ b}> :: t2). split. + * apply clos_rt1n_rtn1. econstructor. + -- apply red_cond_false. + -- simpl. + replace (Cond <{~ b}> :: t2) with ([Cond <{~ b}>] ++ t2) by reflexivity. + apply clos_rtn1_rt1n. apply canonical_extends; assumption. + * inversion HPhi; subst. + unfold PHI; simpl. + rewrite denotB_and, denotB_neg, Bapply_id, intersect_comm. + reflexivity. + - inversion H; subst. + generalize dependent B. + generalize dependent F. + induction i; intros. + + simpl in H1; inversion H1; subst. + exists [Cond <{~ b}>]. split. + * econstructor. + -- apply red_loop_false with (t := []). + -- constructor. + * unfold PHI; simpl. + rewrite Bapply_id, denotB_and, denotB_top, denotB_neg, denot_id_sub. + rewrite intersect_full'. + reflexivity. + + apply loop_helper_step in H1. + destruct H1 as (? & ? & ? & ?). + destruct H2 as (Floop & Bloop & Fbody & Bbody & ? & ? & ? & ?). + inversion H2. simpl in H4, H5. subst. + inversion H0. destruct H4. destruct H5. + assert (InBbody: Inhabited _ Bbody) + by (apply Inhabited_intro with (x := x); assumption). + destruct (IHp Fbody Bbody H3 InBbody) as (tBody & ? & PHIbody). + assert (inBloop: Inhabited _ Bloop) + by (apply Inhabited_intro with (x := Fbody x); assumption). + assert (inLoop: Ensembles.In _ (denot__S <{while b {p}}>) (Floop, Bloop)) + by (apply Fam_intro with (i := i); apply H1). + destruct (IHi Floop Bloop inLoop inBloop H1) as (tLoop & ? & PHIloop). + exists (Cond b :: tBody ++ tLoop). split. + * apply canonical_while. exists (tBody ++ tLoop). left. split. + -- reflexivity. + -- apply concat_sequence; assumption. + * inversion PHIbody; subst; inversion PHIloop; subst. + unfold PHI; simpl. + rewrite acc_subst_concat_comp. + rewrite denotB_and, Bapply_id. + rewrite pc_concat_intersect. + reflexivity. +Qed. + +(* Theorem 2 *) +Theorem big_small_correspondence: forall p, + (exists F B, Ensembles.In _ (denot__S p) (F, B) /\ Inhabited _ B) <-> + exists t, canonical p t /\ feasible t. +Proof. + split; intros. + - destruct H as (F & B & ? & ?). + destruct (big_to_small _ _ _ H H0) as (t & ? & ?). + exists t. split. + + apply H1. + + inversion H2; subst. apply H0. + - destruct H as (t &Hcanon & Hfeas). + specialize (small_to_big _ _ Hcanon Hfeas); intro. + exists (fst (PHI t)). exists (snd (PHI t)). + split; assumption. +Qed. diff --git a/Direct.v b/Direct.v new file mode 100644 index 0000000..55613f4 --- /dev/null +++ b/Direct.v @@ -0,0 +1,190 @@ +From Coq Require Import + String Bool Datatypes Relations Program.Equality Classes.RelationClasses + Relations.Operators_Properties + Logic.FunctionalExtensionality (* for equality of substitutions *) + Ensembles + Init.Datatypes + Lists.List +. +Import ListNotations. + +From BigStepSymbEx Require Import + Expr + Syntax + Maps + SmallStep + BigStep + Correspondence. +Import While. + +Open Scope com_scope. +Open Scope string_scope. +Open Scope list_scope. + +Definition SConfig : Type := Stmt * sub * Bexpr. + +Reserved Notation " c '=>s' c' " (at level 40). + +(* Figure 3 *) +Inductive Sstep : relation SConfig := +| Asgn_step : forall x e sig phi, + (<{ x := e }>, sig , phi) =>s (SSkip, (update sig x (Aapply sig e)), phi) +| IfTrue_step : forall b p1 p2 sig phi, + (<{ if b {p1} {p2} }>, sig, phi) =>s (p1, sig, BAnd phi (Bapply sig b)) +| IfFalse_step : forall b p1 p2 sig phi, + (<{ if b {p1} {p2} }>, sig, phi) =>s (p2 , sig, BAnd phi (BNot (Bapply sig b))) +| WhileTrue_step : forall b p sig phi, + (<{ while b {p} }>, sig, phi) =>s (<{ p ; while b {p}}>, sig, BAnd phi (Bapply sig b)) +| WhileFalse_step : forall b p sig phi, + (<{ while b {p}}>, sig, phi) =>s (SSkip, sig, BAnd phi (BNot (Bapply sig b))) +| Skip_step : forall p sig phi, + (<{skip ; p}>, sig, phi) =>s (p, sig, phi) +| Seq_step : forall p p' q sig sig' phi phi', + (p, sig, phi) =>s (p', sig', phi') -> + (<{p ; q}>, sig, phi) =>s (<{p' ; q}>, sig', phi') + where " c '=>s' c' " := (Sstep c c'). + +Definition multi_Sstep := clos_refl_trans_n1 _ Sstep. +Notation " c '=>*' c' " := (multi_Sstep c c') (at level 40). + +Lemma direct_if_trace_step: forall p p' t t' phi, + red__S (t, p) (t', p') -> + denot__B phi = denot__B (acc_pc t id_sub) -> + (exists phi', (p, acc_subst t id_sub, phi) =>s (p', acc_subst t' id_sub, phi') + /\ denot__B phi' = denot__B (acc_pc t' id_sub)). +Proof. + intros. dependent induction H; subst. + - exists phi. split. + + rewrite acc_subst_asgn_last. constructor. + + rewrite acc_pc_asgn_last; auto. + - exists (BAnd phi (Bapply (acc_subst t id_sub) b)). split. + + rewrite acc_subst_cond_last. + apply IfTrue_step. + + rewrite acc_pc_cond_last, 2 denotB_and, H0. auto. + - exists (BAnd phi (BNot (Bapply (acc_subst t id_sub) b))). split. + + rewrite acc_subst_cond_last. + apply IfFalse_step. + + rewrite acc_pc_cond_last, 2 denotB_and, H0. auto. + - exists (BAnd phi (Bapply (acc_subst t id_sub) b)). split. + + rewrite acc_subst_cond_last. + apply WhileTrue_step. + + rewrite acc_pc_cond_last, 2 denotB_and, H0. auto. + - exists (BAnd phi (BNot (Bapply (acc_subst t id_sub) b))). split. + + rewrite acc_subst_cond_last. + apply WhileFalse_step. + + rewrite acc_pc_cond_last, 2 denotB_and, H0. auto. + - exists phi. split. + + apply Skip_step. + + assumption. + - destruct (IHred__S p0 p'0 t t' eq_refl eq_refl H0) as (phi' & ? & ?). + exists phi'. split; [apply Seq_step|]; assumption. +Qed. + +(* Proposition 1a *) +Lemma direct_if_trace: forall p p' t t' phi, + (t, p) ->* (t', p') -> + denot__B phi = denot__B (acc_pc t id_sub) -> + (exists phi', (p, acc_subst t id_sub, phi) =>* (p', acc_subst t' id_sub, phi') + /\ denot__B phi' = denot__B (acc_pc t' id_sub)). +Proof. + intros. dependent induction H. + - exists phi. split. + + constructor. + + auto. + - destruct y. + destruct (IHclos_refl_trans_n1 p s t t0 eq_refl eq_refl H1) as (phi' & ? & ?). + destruct (direct_if_trace_step _ _ _ _ phi' H H3) as (phi'' & ? & ?). + exists phi''. split. + + econstructor. + * apply H4. + * apply H2. + + auto. +Qed. + +Lemma trace_if_direct_step: forall p p' t sig phi sig' phi', + (p, sig, phi) =>s (p', sig', phi') -> + acc_subst t id_sub = sig -> + denot__B (acc_pc t id_sub) = denot__B phi -> + exists t', red__S (t, p) (t', p') + /\ acc_subst t' id_sub = sig' + /\ denot__B (acc_pc t' id_sub) = denot__B phi'. +Proof. + intros. dependent induction H; subst. + - exists (t ++ [Asgn x e]). repeat split. + + constructor. + + rewrite acc_subst_asgn_last. auto. + + rewrite acc_pc_asgn_last. auto. + - exists (t ++ [Cond b]). repeat split. + + constructor. + + rewrite acc_subst_cond_last. auto. + + rewrite acc_pc_cond_last, 2 denotB_and, H1. auto. + - exists (t ++ [Cond <{~ b}>]). repeat split. + + constructor. + + rewrite acc_subst_cond_last. auto. + + rewrite acc_pc_cond_last, 2 denotB_and, H1. auto. + - exists (t ++ [Cond b]). repeat split. + + constructor. + + rewrite acc_subst_cond_last. auto. + + rewrite acc_pc_cond_last, 2 denotB_and, H1. auto. + - exists (t ++ [Cond <{~ b}>]). repeat split. + + constructor. + + rewrite acc_subst_cond_last. auto. + + rewrite acc_pc_cond_last, 2 denotB_and, H1. auto. + - exists t. repeat split. + + constructor. + + assumption. + - destruct (IHSstep p0 p'0 (acc_subst t id_sub) phi sig' phi' JMeq_refl JMeq_refl eq_refl H1) + as (t' & ? & ? & ?). + exists t'. repeat split; [constructor| |]; assumption. +Qed. + +(* Proposition 1b *) +Lemma trace_if_direct: forall p p' t sig phi sig' phi', + (p, sig, phi) =>* (p', sig', phi') -> + acc_subst t id_sub = sig -> + denot__B (acc_pc t id_sub) = denot__B phi -> + exists t', (t, p) ->* (t', p') + /\ acc_subst t' id_sub = sig' + /\ denot__B (acc_pc t' id_sub) = denot__B phi'. +Proof. + intros. dependent induction H. + - exists t. repeat split; + [constructor| |]; assumption. + - destruct y, p0. + destruct (IHclos_refl_trans_n1 _ _ _ _ _ _ JMeq_refl JMeq_refl H1 H2) + as (t' & ? & ? & ?). + destruct (trace_if_direct_step _ _ _ _ _ _ _ H H4 H5) as (t'' & ? & ? & ?). + exists t''. repeat split; try assumption. + + econstructor; [apply H6 | apply H3]. +Qed. + +(* Corollary 1 *) +Corollary correctness: forall p sig phi, + (p, id_sub, BTrue) =>* (SSkip, sig, phi) -> + forall V, Beval V phi = true -> + denot_fun p V = Some (denot_sub sig V). +Proof. + intros. apply (trace_if_direct _ _ []) in H; auto. + destruct H as (t' & Hcomp & ? & ?). + assert (tfeasible: feasible t'). { exists V. rewrite H1. apply H0. } + specialize (small_to_big _ _ Hcomp tfeasible). intro. + destruct (correct p (denot_sub (acc_subst t' id_sub)) (denot__B (acc_pc t' id_sub)) V H2) + as (V' & <- & ?). + - rewrite H1. apply H0. + - rewrite <- H. apply H3. +Qed. + +(* Corollary 2 *) +Corollary completeness: forall p V V', + denot_fun p V = Some V' -> + exists sig phi, (p, id_sub, BTrue) =>* (SSkip, sig, phi) /\ Beval V phi = true. +Proof. + intros. destruct (complete _ _ _ H) as (F & B & ? & ? & ?). + assert (Inhabited _ B) by (exists V; auto). + destruct (big_to_small _ _ _ H0 H3) as (t & ? & ?). + destruct (direct_if_trace _ _ _ _ BTrue H4) as (phi & ? & ?); auto. + exists (acc_subst t id_sub), phi. split. + - apply H6. + - inversion H5; subst. + rewrite <- H7 in H2. apply H2. +Qed. diff --git a/Expr.v b/Expr.v new file mode 100644 index 0000000..316f648 --- /dev/null +++ b/Expr.v @@ -0,0 +1,30 @@ +(** * Expressions *) +From Coq Require Import Strings.String. +From Coq Require Import Bool.Bool. +From Coq Require Import Init.Nat. + +Inductive Aexpr : Type := +| AConst (n:nat) +| AVar (x:string) +| APlus (a1 a2:Aexpr). + +Inductive Bexpr : Type := +| BTrue +| BFalse +| BNot (b:Bexpr) +| BAnd (b1 b2:Bexpr) +| BLeq (a1 a2:Aexpr). + +Coercion AVar : string >-> Aexpr. +Coercion AConst : nat >-> Aexpr. + +Declare Custom Entry com. +Declare Scope com_scope. + +Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope. +Notation "( x )" := x (in custom com, x at level 99) : com_scope. +Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope. +Notation "x + y" := (APlus x y) (in custom com at level 70, no associativity). +Notation "x <= y" := (BLeq x y) (in custom com at level 70, no associativity). +Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity). +Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity). diff --git a/Limits.v b/Limits.v new file mode 100644 index 0000000..6385da3 --- /dev/null +++ b/Limits.v @@ -0,0 +1,73 @@ +From Coq Require Import + Init.Datatypes + Psatz + ZArith. + +(* We need Constructive Definite Description – a relatively weak omniscience principle *) +(*https://coq.inria.fr/stdlib/Coq.Logic.Description.html*) +(*https://www.cs.princeton.edu/courses/archive/fall07/cos595/stdlib/html/Coq.Logic.ChoiceFacts.html*) +From Coq Require Import Classical Description. + +(* Trick from Leroy *) +(*https://xavierleroy.org/cdf-mech-sem/CDF.Divergence.html*) +Inductive lessdef {A: Type}: option A -> option A -> Prop := +| lessdef_none: forall oa, lessdef None oa +| lessdef_some: forall a, lessdef (Some a) (Some a). + +Notation "x <<= y" := (lessdef x y) (at level 70, no associativity). + +#[export] +Hint Constructors lessdef : lessdef. + +Lemma lessdef_refl {X:Type}: forall (x:option X), x <<= x. +Proof. destruct x; constructor. Qed. + +Definition option_bind {X Y: Type} (m : option X) (f: X -> option Y): option Y := + match m with None => None | Some x => f x end. + +Definition option_compose {X Y Z: Type} (f: X -> option Y) (g: Y -> option Z): X -> option Z := + fun x => option_bind (f x) g. + +Definition option_lift {X Y: Type} (f: X -> Y): X -> option Y := fun x => Some (f x). + +Lemma option_bind_mono: forall (X Y: Type) (x x': option X) (f f': X -> option Y), + x <<= x' -> (forall x, f x <<= f' x) -> option_bind x f <<= option_bind x' f'. +Proof. intros. destruct H; cbn; auto with lessdef. Qed. + +Lemma option_inversion {X Y: Type} {x: option X} {f: X -> option Y} {y: Y}: + option_bind x f = Some y -> + exists x', x = Some x' /\ f x' = Some y. +Proof. + destruct x; simpl; intros. + - exists x. split; auto. + - inversion H. +Qed. + +Section LIMIT. + + Context {A: Type} (f: nat -> option A). + + Hypothesis f_mono: forall i j, i <= j -> f i <<= f j. + + Lemma limit_exists: + { lim : option A | exists i, forall j, i <= j -> f j = lim }. + Proof. + apply constructive_definite_description. + destruct (classic (forall i, f i = None)) as [DIV|TERM]. + - exists None; split. + + exists O; auto. + + intros lim (i & LIM). rewrite <- (DIV i). apply LIM; lia. + - apply not_all_ex_not in TERM. destruct TERM as (i & TERM). + exists (f i); split. + + exists i; intros. destruct (f_mono i j H). congruence. auto. + + intros lim (i2 & LIM2). set (j := Nat.max i i2). + rewrite <- (LIM2 j) by lia. + destruct (f_mono i j). lia. congruence. auto. + Qed. + + Definition limit : option A := proj1_sig limit_exists. + + Lemma limit_charact: exists i, forall j, i <= j -> f j = limit. + Proof. unfold limit. apply proj2_sig. Qed. + +End LIMIT. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..74b8a7b --- /dev/null +++ b/Makefile @@ -0,0 +1,953 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # Copyright INRIA, CNRS and contributors ## +## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQNATIVE ?= "$(COQBIN)coqnative" +COQDEP ?= "$(COQBIN)coqdep" +COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" +COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= +FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +TGTS ?= + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) +COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + +# findlib files installation +FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" +FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" + +# we need to move out of sight $(METAFILE) otherwise findlib thinks the +# package is already installed +findlib_install = \ + $(HIDE)if [ "$(METAFILE)" ]; then \ + $(FINDLIBPREINST) && \ + mv "$(METAFILE)" "$(METAFILE).skip" ; \ + "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ + rc=$$?; \ + mv "$(METAFILE).skip" "$(METAFILE)"; \ + exit $$rc; \ + fi +findlib_remove = \ + $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ + "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ + fi + + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" +# +# in Makefile.local +# +############################################################################### + + + + +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters. +# To add additional flags to coq, coqchk or coqdoc, set the +# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. +# To overwrite the default choice and set your own flags entirely, set the +# {COQ,COQCHK,COQDOC}FLAGS variable. + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +OPT?= + +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + +# these variables are meant to be overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# Find the last argument of the form "-native-compiler FLAG" +COQUSERNATIVEFLAG:=$(strip \ +$(subst -native-compiler-,,\ +$(lastword \ +$(filter -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))))) + +COQFILTEREDEXTRAFLAGS:=$(strip \ +$(filter-out -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))) + +COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) + +ifeq '$(COQACTUALNATIVEFLAG)' 'yes' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="yes" +else +ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="no" +else + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" + COQDONATIVE="no" +endif +endif + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) +COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) +COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) + +COQDOCLIBS?=$(COQLIBS_NOML) + +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) +COQMAKEFILE_VERSION:=8.16.1 + +# COQ_SRC_SUBDIRS is for user-overriding, usually to add +# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for +# Coq's own core libraries, which should be replaced by ocamlfind +# options at some point. +COQ_SRC_SUBDIRS?= +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) + +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing +else +TIMING_EXT=timing +endif +endif +else +TIMING_ARG= +endif + +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +VDFILE := .Makefile.d + +ALLSRCFILES := \ + $(MLGFILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + +VO = vo +VOS = vos + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(MLGFILES:.mlg=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .mlg file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) + +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMXSFILES) # to be removed when we remove legacy loading +FINDLIBFILESTOINSTALL = \ + $(CMIFILESTOINSTALL) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all + +post-all:: + @# Extension point +.PHONY: post-all + +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all + +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONY: real-all.timing.diff + +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + +# FIXME, see Ralf's bugreport +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +# quick2vo is undocumented +quick2vo: + $(HIDE)make -j $(J) vio + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ +.PHONY: validate + +only: $(TGTS) +.PHONY: only + +# Documentation targets ####################################################### + +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) + +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html + +all-gal.ps: GAL=-g +all-gal.ps: all.ps + +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf + +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @echo 'Do not do "make clean" until you are sure that everything went well!' + @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +.PHONY: beautify + +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +# findlib needs the package to not be installed, so we remove it before +# installing it (see the call to findlib_remove) +install: META + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + $(call findlib_remove) + $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) + $(HIDE)$(MAKE) install-extra -f "$(SELF)" +install-extra:: + @# Extension point +.PHONY: install install-extra + +META: $(METAFILE) + $(HIDE)if [ "$(METAFILE)" ]; then \ + cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + fi + +install-byte: + $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done +.PHONY: install-doc + +uninstall:: + @# Extension point + $(call findlib_remove) + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" ;\ + done + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ + done + +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +clean:: + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -f META + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + +$(VOFILES): %.vo: %.v | $(VDFILE) + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $@ + $(HIDE)$(COQNATIVE) $(COQLIBS) $@ +endif + +# FIXME ?merge with .vo / .vio ? +$(GLOBFILES): %.glob: %.v + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< + +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifndef MAKECMDGOALS + -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + +$(VDFILE): _CoqProject $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) + +# Misc ######################################################################## + +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte + +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.local or include Makefile.conf) + @echo 'COQLIB = $(COQLIB)' + @echo 'COQCORELIB = $(COQCORELIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIB = $(COQLIBS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQCORELIB)' >> .merlin + $(HIDE)echo 'S $(COQCORELIB)' >> .merlin + $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ + echo 'B $(COQCORELIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all + +# Users can create Makefile.local-late to hook into double-colon rules +# or add other needed Makefile code, using defined +# variables if necessary. +-include Makefile.local-late + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/Makefile.conf b/Makefile.conf new file mode 100644 index 0000000..5a78ac2 --- /dev/null +++ b/Makefile.conf @@ -0,0 +1,64 @@ +# This configuration file was generated by running: +# coq_makefile -f _CoqProject -o Makefile + + +############################################################################### +# # +# Project files. # +# # +############################################################################### + +COQMF_VFILES = Limits.v Expr.v Maps.v Syntax.v BigStep.v SmallStep.v Direct.v Correspondence.v +COQMF_MLIFILES = +COQMF_MLFILES = +COQMF_MLGFILES = +COQMF_MLPACKFILES = +COQMF_MLLIBFILES = +COQMF_METAFILE = +COQMF_CMDLINE_VFILES = + +############################################################################### +# # +# Path directives (-I, -R, -Q). # +# # +############################################################################### + +COQMF_OCAMLLIBS = +COQMF_SRC_SUBDIRS = +COQMF_COQLIBS = -R . BigStepSymbEx +COQMF_COQLIBS_NOML = -R . BigStepSymbEx +COQMF_CMDLINE_COQLIBS = + +############################################################################### +# # +# Coq configuration. # +# # +############################################################################### + +COQMF_COQLIB=/home/aqissiaq/.opam/default/lib/coq/ +COQMF_COQCORELIB=/home/aqissiaq/.opam/default/lib/coq/../coq-core/ +COQMF_DOCDIR=/home/aqissiaq/.opam/default/doc/coq/ +COQMF_OCAMLFIND=/home/aqissiaq/.opam/default/bin/ocamlfind +COQMF_CAMLFLAGS=-thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence +COQMF_WARN=-warn-error +a-3 +COQMF_HASNATDYNLINK=true +COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax +COQMF_COQ_NATIVE_COMPILER_DEFAULT=no +COQMF_WINDRIVE= + +############################################################################### +# # +# Native compiler. # +# # +############################################################################### + +COQMF_COQPROJECTNATIVEFLAG = + +############################################################################### +# # +# Extra variables. # +# # +############################################################################### + +COQMF_OTHERFLAGS = +COQMF_INSTALLCOQDOCROOT = BigStepSymbEx diff --git a/Maps.v b/Maps.v new file mode 100644 index 0000000..5d69cbe --- /dev/null +++ b/Maps.v @@ -0,0 +1,184 @@ +(** * Substitutions and Valuations *) + +From Coq Require Import Strings.String. +From Coq Require Import Bool.Bool. +From Coq Require Import Init.Nat. +From Coq Require Import Arith.Arith. +From Coq Require Import Arith.EqNat. Import Nat. +From Coq Require Import Logic.FunctionalExtensionality. (* for equality of substitutions *) + +From BigStepSymbEx Require Import Expr. + +Class HasEqb (X: Type) := + { eqb : X -> X -> bool ; + eqb_spec : forall x y, reflect (x = y) (eqb x y) + }. + +#[global] Instance string_eqb: HasEqb string := + { eqb := String.eqb ; + eqb_spec := String.eqb_spec + }. + +#[global] Instance nat_eqb: HasEqb nat := + { eqb := Nat.eqb ; + eqb_spec := Nat.eqb_spec + }. + +Lemma eqb_refl {X:Type} `{HasEqb X}: forall (x:X), eqb x x = true. +Proof. intros. destruct (eqb_spec x x). + - reflexivity. + - contradiction. +Qed. + +Lemma eqb_neq {X:Type} `{HasEqb X}: forall x y, eqb x y = false <-> x <> y. +Proof. intros. destruct (eqb_spec x y); split; + [discriminate | contradiction | auto | auto ]. +Qed. + +Section TotalMaps. + Context {X A: Type} + `{HasEqb X}. + + Definition total_map: Type := X -> A. + + Definition update (s: total_map) (x:X) (e:A) : total_map := + fun y => if eqb x y then e else s y. + + Notation "x '!->' v ';' m" := (update m x v) (at level 100, v at next level, right associativity). + + Definition empty_map (x:A): total_map := fun _ => x. + Notation "'_' '!->' v" := (empty_map v) (at level 100, right associativity). + + Lemma apply_empty : forall x v, + (_ !-> v) x = v. + Proof. intros. unfold empty_map. reflexivity. Qed. + + Lemma update_eq : forall x m v, + (x !-> v ; m) x = v. + Proof. intros. unfold update. rewrite eqb_refl. reflexivity. Qed. + + Theorem update_neq : forall (m : total_map) x y v, + x <> y -> + (x !-> v ; m) y = m y. + Proof. + intros. unfold update. destruct (eqb_spec x y). + - contradiction. + - reflexivity. + Qed. + + Lemma equal_maps {m m' : total_map} : + m = m' -> forall x, m x = m' x. + Proof. intros. subst. reflexivity. Qed. + + Lemma update_shadow : forall (m : total_map) x v1 v2, + (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m). + Proof. + intros. extensionality y. unfold update. + destruct (eqb x y); reflexivity. + Qed. + + Lemma update_comm: forall m x1 x2 v1 v2, + x1 <> x2 -> (x1 !-> v1 ; x2 !-> v2 ; m) = (x2 !-> v2 ; x1 !-> v1 ; m). + Proof. + intros. extensionality y. unfold update. + destruct (eqb_spec x1 y); destruct (eqb_spec x2 y); + try reflexivity. + exfalso. apply H0. rewrite e, e0. reflexivity. + Qed. +End TotalMaps. + +(* notation is not allowed to escape sections atm *) +(*https://github.com/coq/coq/issues/11672*) +Notation "x '!->' v ';' m" := (update m x v) (at level 100, v at next level, right associativity). +Notation "'_' '!->' v" := (empty_map v) (at level 100, right associativity). + +(* substitions map to (Arithmetic) expressions*) +Definition sub : Type := @total_map string Aexpr. +Definition id_sub : sub := fun x => x. + +(* valuations map to concrete values *) +Definition Valuation := @total_map string nat. + +Fixpoint Aapply (s:sub) (e:Aexpr) : Aexpr := + match e with + | AConst n => AConst n + | AVar x => s x + | APlus a1 a2 => APlus (Aapply s a1) (Aapply s a2) + end. + +Lemma Aapply_id : forall e, + Aapply id_sub e = e. +Proof. + induction e; try reflexivity. + simpl. rewrite IHe1. rewrite IHe2. reflexivity. +Qed. + +Fixpoint Bapply (s:sub) (e:Bexpr) : Bexpr := + match e with + | BTrue => BTrue + | BFalse => BFalse + | BNot b => BNot (Bapply s b) + | BAnd b1 b2 => BAnd (Bapply s b1) (Bapply s b2) + | BLeq a1 a2 => BLeq (Aapply s a1) (Aapply s a2) + end. + +Lemma Bapply_id : forall e, + Bapply id_sub e = e. +Proof. + induction e; simpl; + try (rewrite IHe); + try (rewrite IHe1; rewrite IHe2); + try (repeat rewrite Aapply_id); + try reflexivity. +Qed. + +Fixpoint Aeval (V:Valuation) (e:Aexpr) : nat := + match e with + | AConst n => n + | AVar x => V x + | APlus a1 a2 => (Aeval V a1) + (Aeval V a2) + end. + +Fixpoint Beval (V:Valuation) (e:Bexpr) : bool := + match e with + | BTrue => true + | BFalse => false + | BNot b => negb (Beval V b) + | BAnd b1 b2 => (Beval V b1) && (Beval V b2) + | BLeq a1 a2 => (Aeval V a1) <=? (Aeval V a2) + end. + +(** We can update a valuation with a substitution by composition + and prove some useful properties *) + +Definition Comp (V:Valuation) (s:sub) : Valuation := + fun x => Aeval V (s x). + +Lemma comp_sub : forall V s e, + Aeval (Comp V s) e = Aeval V (Aapply s e). +Proof. + induction e; simpl; + try (rewrite IHe1; rewrite IHe2); reflexivity. +Qed. + +Lemma comp_subB : forall V s e, + Beval (Comp V s) e = Beval V (Bapply s e). +Proof. + induction e; simpl; + try (rewrite IHe1; rewrite IHe2); + try (rewrite IHe); + try (repeat (rewrite comp_sub)); + reflexivity. +Qed. + +Lemma asgn_sound : forall V s x e, + Comp V (update s x (Aapply s e)) = update (Comp V s) x (Aeval (Comp V s) e). +Proof. intros. extensionality y. + unfold Comp. unfold update. destruct (eqb x y); + try (rewrite <- comp_sub; unfold Comp); + reflexivity. +Qed. + +Lemma comp_id : forall V, + Comp V id_sub = V. +Proof. intros. extensionality x. reflexivity. Qed. diff --git a/README.md b/README.md index 39999ce..3986d4d 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,27 @@ -# ICTAC-DenotSymbEx -Coq mechanization of "Denotational Semantics for Symbolic Execution" for ICTAC23 submission +# ICTAC: Denotational Semantics for Symbolic Execution +Coq mechanization of "Denotational Semantics for Symbolic Execution" for ICTAC23 submission. + +## Contents +### Main results + - [BigStep](./BigStep.v) covers section 2-3, culminating in Theorem 1: `concrete_symbolic_correspondence` + - [SmallStep](./SmallStep.v) defines and describes the small-step trace semantics of section 4, and + - [Correspondence](./Correspondence.v) proves Theorem 2: `big_small_correspondence` + - [Direct](./Direct.v) proves Proposition 1 (`trace_if_direct` and `direct_if_trace`) and its corollaries `correctness` and `completeness`. + +### Auxilliary materials + - [Expr](./Expr.v) contains the syntax of expressions, and + - [Syntax](./Syntax.v) the syntax of our toy language WHILE + - [Maps](./Maps.v) contains definitions and useful lemmas about total maps used to reason about substitutions and valuations + - [Limits](./Limits.v) contains the use of constructive description to handle non-termination + - Finally, [BigStepExamples](./BigStepExamples.v) contains some examples runs of the big step semantics + +## Build +The included Makefile (created for Coq 8.16.1) should allow just +```sh +make +``` + +To update the Makefile use +```sh +coq_makefile -f _CoqProject -o Makefile +``` diff --git a/SmallStep.v b/SmallStep.v new file mode 100644 index 0000000..171857f --- /dev/null +++ b/SmallStep.v @@ -0,0 +1,578 @@ +From Coq Require Import + String Bool Datatypes Relations Program.Equality Classes.RelationClasses + Relations.Operators_Properties + Logic.FunctionalExtensionality (* for equality of substitutions *) + Ensembles + Init.Datatypes + Lists.List +. +Import ListNotations. + +From BigStepSymbEx Require Import + Expr + Syntax + Maps +. +Import While. + +Open Scope com_scope. +Open Scope string_scope. +Open Scope list_scope. + +Section RelationHelpers. + Variable A: Type. + Variable R: relation A. + + Lemma clos_rtn1_rt1n: forall x y, + clos_refl_trans_n1 _ R x y -> clos_refl_trans_1n _ R x y. + Proof. intros. apply clos_rt_rt1n. apply clos_rtn1_rt. apply H. Qed. + + Lemma clos_rt1n_rtn1: forall x y, + clos_refl_trans_1n _ R x y -> clos_refl_trans_n1 _ R x y. + Proof. intros. apply clos_rt_rtn1. apply clos_rt1n_rt. apply H. Qed. + + Lemma clos_rt1n_rtn1_iff: forall x y, + clos_refl_trans_1n _ R x y <-> clos_refl_trans_n1 _ R x y. + Proof. split; [apply clos_rt1n_rtn1 | apply clos_rtn1_rt1n]. Qed. + + Global Instance clos_rtn1_trans: Transitive (clos_refl_trans_n1 _ R). + Proof. + intros x y z H0 H1. + apply clos_rtn1_rt in H0, H1. + apply clos_rt_rtn1. + apply rt_trans with (y := y); assumption. + Qed. +End RelationHelpers. + +Section ListHelpers. + Variable A : Type. + + Lemma app_tail_inj: forall (t1 t2 t2': list A), + t1 ++ t2 = t1 ++ t2' -> t2 = t2'. + Proof. + induction t1; intros. + - apply H. + - simpl in H. inversion H. + apply IHt1; assumption. + Qed. + + Lemma app_nil_unique_r: forall (t1 t2: list A), + t1 = t1 ++ t2 -> t2 = []. + Proof. + induction t1; intros. + - rewrite H. auto. + - inversion H. apply IHt1; assumption. + Qed. + + Lemma app_nil_unique_l: forall (t1 t2: list A), + t1 = t2 ++ t1 -> t2 = []. + Proof. + induction t1; intros. + - rewrite app_nil_r in H. auto. + - destruct t2; auto. + inversion H; subst. replace (t2 ++ a0 :: t1) with ((t2 ++ [a0]) ++ t1) in H2. + + apply IHt1 in H2. destruct (app_eq_nil _ _ H2); subst; assumption. + + rewrite <- app_assoc. auto. + Qed. +End ListHelpers. + +Inductive trace_step: Type := +| Asgn (x:string) (e:Aexpr) +| Cond (b:Bexpr). + +Definition trace__S := list trace_step. + +Inductive red__S: (trace__S * Stmt) -> (trace__S * Stmt) -> Prop := +| red_asgn: forall t x e, + red__S (t, <{ x := e }>) (t ++ [Asgn x e], SSkip) +| red_cond_true: forall t b p1 p2, + red__S (t, <{ if b {p1} {p2} }>) (t ++ [Cond b], p1) +| red_cond_false: forall t b p1 p2, + red__S (t, <{ if b {p1} {p2} }>) (t ++ [Cond (BNot b)], p2) +| red_loop_true: forall t b p, + red__S (t, <{ while b {p} }>) (t ++ [Cond b], <{p ; while b {p}}>) +| red_loop_false: forall t b p, + red__S (t, <{ while b {p} }>) (t ++ [Cond (BNot b)], SSkip) +| red_skip: forall t p, + red__S (t, <{skip ; p}>) (t, p) +| red_seq: forall p p' t t' q, + red__S (t, p) (t', p') -> + red__S (t, <{p ; q}>) (t', <{p' ; q}>) +. +Definition red_star__S := clos_refl_trans_n1 _ red__S. + +Notation " c '->*' c'" := (red_star__S c c') (at level 40). + +Lemma trace_extends_step: forall p q s t, + red__S (s, p) (t, q) -> exists t', t = s ++ t'. +Proof. + intros. dependent induction H. + - exists [Asgn x e]. reflexivity. + - exists [Cond b]. reflexivity. + - exists [Cond <{~ b}>]. reflexivity. + - exists [Cond b]. reflexivity. + - exists [Cond <{~ b}>]. reflexivity. + - exists []. rewrite app_nil_r. reflexivity. + - destruct (IHred__S p0 p' s t) as [t' H']; try reflexivity. + exists t'. apply H'. +Qed. + +(* Lemma 3 *) +Lemma trace_extends: forall p q s t, + (s, p) ->* (t, q) -> exists t', t = s ++ t'. +Proof. + intros. dependent induction H. + - exists []. rewrite app_nil_r. reflexivity. + - destruct y. + destruct (trace_extends_step _ _ _ _ H) as [tStep Hstep]. + destruct (IHclos_refl_trans_n1 p s0 s t0 eq_refl eq_refl) as [tIH IH]. + exists (tIH ++ tStep). subst. rewrite app_assoc. reflexivity. +Qed. + +Lemma trace_extends_cons: forall p q x s t, + (x :: s, p) ->* (t, q) -> exists t', t = x :: t'. +Proof. + intros. destruct (trace_extends _ _ (x::s) _ H); subst. + exists (s ++ x0). reflexivity. +Qed. + +Lemma trans_append: forall p q r s t, + ([], p) ->* (s, q) -> + (s, q) ->* (t, r) -> + exists t', ([], p) ->* (s ++ t', r) /\ t = s ++ t'. +Proof. + intros. + destruct (trace_extends _ _ _ _ H0) as [t' Happ]. + exists t'. rewrite Happ in H0. split. + - transitivity (s, q); assumption. + - assumption. +Qed. + +Definition canonical (p: Stmt): trace__S -> Prop := + fun t => ([], p) ->* (t, SSkip). + +Lemma empty_to_empty: forall p q t0, + (t0, p) ->* ([], q) -> t0 = []. +Proof. + intros. destruct (trace_extends _ _ _ _ H). + destruct x, t0; + try reflexivity. + - rewrite app_nil_r in H0. apply nil_cons in H0; contradiction. + - apply app_cons_not_nil in H0. contradiction. +Qed. + +Lemma empty_to_empty_step: forall p q t0, + red__S (t0, p) ([], q) -> t0 = []. +Proof. + intros. apply (empty_to_empty p q). + econstructor. + - apply H. + - constructor. +Qed. + +Lemma skip_terminates: forall t y, + ~ (red__S (t, SSkip) y). +Proof. + intros t y contra. + inversion contra; subst. +Qed. + +Lemma skip_non_productive: forall p s t, + (s, SSkip) ->* (t, p) -> t = s /\ p = SSkip. +Proof. + intros. apply clos_rtn1_rt1n in H. inversion H; subst. + - split; reflexivity. + - exfalso. apply (skip_terminates s y H0). +Qed. + +Lemma prefix_step: forall s t p q, + red__S (s, p) (t, q) -> + forall t0, red__S (t0 ++ s, p) (t0 ++ t, q). +Proof. + intros. dependent induction H; + try (rewrite app_assoc; constructor). + - apply red_skip. + - apply red_seq. apply IHred__S; reflexivity. +Qed. + +Lemma prefix_star: forall s t p q, + (s, p) ->* (t, q) -> + forall t0, (t0 ++ s, p) ->* (t0 ++ t, q). +Proof. + intros. dependent induction H. + - constructor. + - destruct y. apply prefix_step with (t0 := t0) in H. + specialize (IHclos_refl_trans_n1 s t1 p s0 eq_refl eq_refl t0). + econstructor; + [apply H | apply IHclos_refl_trans_n1]. +Qed. + +Lemma canonical_extends: forall p s t, + canonical p t -> (s, p) ->* (s ++ t, SSkip). +Proof. + intros. + specialize (prefix_star _ _ _ _ H s). simpl; intros. + rewrite app_nil_r in H0; assumption. +Qed. + +Lemma sequence_star: forall p p' t t' q, + (t, p) ->* (t', p') -> + (t, <{p ; q}>) ->* (t', <{p' ; q}>). +Proof. + intros. dependent induction H. + - constructor. + - destruct y. + econstructor. + + apply red_seq. apply H. + + apply (IHclos_refl_trans_n1 p s t t0); reflexivity. +Qed. + +Lemma prefix_irrelevant_step: forall x t t' p p', + red__S (x :: t, p) (x :: t', p') -> + red__S (t, p) (t', p'). +Proof. + intros. dependent induction H; + try constructor. + apply (IHred__S x); reflexivity. +Qed. + +Lemma prefix_irrelevant_cons: forall x t t' p p', + (x :: t, p) ->* (x :: t', p') -> + (t, p) ->* (t', p'). +Proof. + intros. dependent induction H; subst. + - constructor. + - destruct y. apply trace_extends_cons in H0. + destruct H0; subst. + apply prefix_irrelevant_step in H. + econstructor. + + apply H. + + apply (IHclos_refl_trans_n1 x); reflexivity. +Qed. + +Lemma prefix_irrelevant: forall s t t' p p', + (s ++ t, p) ->* (s ++ t', p') -> + (t, p) ->* (t', p'). +Proof. + induction s; intros. + - apply H. + - simpl in H. apply prefix_irrelevant_cons in H. + apply IHs. apply H. +Qed. + +Lemma canonical_skip: forall t, canonical SSkip t <-> t = []. +Proof. + split; intros. + - apply clos_rtn1_rt in H. apply clos_rt_rt1n in H. + inversion H; subst. + + reflexivity. + + inversion H0; subst. + - subst. constructor. +Qed. + +Lemma canonical_asgn: forall t x e, canonical <{x := e}> t <-> t = [Asgn x e]. +Proof. + split; intros. + - apply clos_rtn1_rt1n in H. inversion H; subst. + inversion H0; subst. apply clos_rt1n_rtn1 in H1. + destruct (skip_non_productive _ _ _ H1). + assumption. + - subst. econstructor. + + apply red_asgn with (t := []). + + constructor. +Qed. + +Lemma canonical_if: forall b p1 p2 t, + canonical <{if b {p1} {p2}}> t <-> exists t', + (t = [Cond b] ++ t' /\ canonical p1 t') + \/ (t = [Cond <{ ~b }>] ++ t' /\ canonical p2 t'). +Proof. + split; intros. + - apply clos_rtn1_rt1n in H. inversion H. inversion H0; subst. + + apply clos_rt1n_rtn1 in H1. + assert (([], <{if b {p1}{p2}}>) ->* ([Cond b], p1)). { + econstructor. apply H0. constructor. } + destruct (trans_append _ _ _ _ _ H2 H1) as (t' & Hcomp & ?). + exists t'. left. split. + * assumption. + * apply (prefix_irrelevant [Cond b]). + rewrite H3 in H1. simpl in H1. + simpl. apply H1. + + apply clos_rt1n_rtn1 in H1. + assert (([], <{if b {p1}{p2}}>) ->* ([Cond <{~b}>], p2)). { + econstructor. apply H0. constructor. } + destruct (trans_append _ _ _ _ _ H2 H1) as (t' & Hcomp & ?). + exists t'. right. split. + * assumption. + * apply (prefix_irrelevant [Cond <{~b}>]). + rewrite H3 in H1. simpl in H1. + simpl. apply H1. + - destruct H as [t' H]. destruct H. + + destruct H; subst. + apply clos_rt1n_rtn1. econstructor. + * apply red_cond_true. + * apply clos_rtn1_rt1n. apply (prefix_star _ _ _ _ H0 [Cond b]). + + destruct H; subst. + apply clos_rt1n_rtn1. econstructor. + * apply red_cond_false. + * apply clos_rtn1_rt1n. apply (prefix_star _ _ _ _ H0 [Cond <{~b}>]). +Qed. + +Lemma canonical_while: forall b p t, + canonical <{while b {p}}> t <-> exists t', + (t = [Cond b] ++ t' /\ canonical <{p ; while b {p}}> t') + \/ (t = [Cond <{ ~b }>]). +Proof. + split; intros. + - apply clos_rtn1_rt1n in H. inversion H. inversion H0; subst. + + apply clos_rt1n_rtn1 in H1. + assert (([], <{while b {p}}>) ->* ([Cond b], <{p ; while b {p}}>)). { + econstructor. apply H0. constructor. } + destruct (trans_append _ _ _ _ _ H2 H1) as (t' & Hcomp & ?). + exists t'. left. split. + * assumption. + * apply (prefix_irrelevant [Cond b]). + rewrite H3 in H1. simpl in H1. + simpl. apply H1. + + exists [Cond <{~ b}>]. right. + apply clos_rt1n_rtn1 in H1. + apply skip_non_productive in H1. + destruct H1; subst. + reflexivity. + - destruct H as [t' H]. destruct H. + + destruct H; subst. + apply clos_rt1n_rtn1. econstructor. + * apply red_loop_true. + * apply clos_rtn1_rt1n. apply (prefix_star _ _ _ _ H0 [Cond b]). + + subst. + apply clos_rt1n_rtn1. econstructor. + * apply red_loop_false. + * constructor. +Qed. + +(* Lemma 5i *) +Lemma concat_sequence: forall p q s t, + canonical p s -> canonical q t -> + canonical <{p ; q}> (s ++ t). +Proof. + intros. apply clos_rt_rtn1. apply rt_trans with (y := (s, <{skip ; q}>)). + - apply clos_rtn1_rt. apply sequence_star. apply H. + - apply clos_rt1n_rt. econstructor. + + apply red_skip. + + apply clos_rt_rt1n. apply clos_rtn1_rt. + specialize (prefix_star _ _ _ _ H0 s). intros. + rewrite app_nil_r in H1. apply H1. +Qed. + +Lemma sequence_splits_step: forall p p' q s t u, + red__S (s, <{p ; q}>) (t, <{p' ; q}>) -> + (t, <{p' ; q}>) ->* (u, SSkip) -> + exists t', + u = t ++ t' + /\ ([], <{p' ; q}>) ->* (t', SSkip). +Proof. + intros. inversion H; subst. + - apply seq_discriminate2 in H6. contradiction. + - inversion H2; subst. + + destruct (trace_extends _ _ _ _ H0); subst. + exists x0. split. + * reflexivity. + * replace (s ++ [Asgn x e]) with ((s ++ [Asgn x e]) ++ []) in H0 + by (rewrite app_nil_r; reflexivity). + replace (((s ++ [Asgn x e]) ++ []) ++ x0) with ((s ++ [Asgn x e]) ++ x0) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant (s ++ [Asgn x e]) [] x0 _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace (s ++ [Cond b]) with ((s ++ [Cond b]) ++ []) in H0 + by (rewrite app_nil_r; reflexivity). + replace (((s ++ [Cond b]) ++ []) ++ x) with ((s ++ [Cond b]) ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant (s ++ [Cond b]) [] x _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace (s ++ [Cond <{~b}>]) with ((s ++ [Cond <{~b}>]) ++ []) in H0 + by (rewrite app_nil_r; reflexivity). + replace (((s ++ [Cond <{~b}>]) ++ []) ++ x) with ((s ++ [Cond <{~b}>]) ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant (s ++ [Cond <{~b}>]) [] x _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace (s ++ [Cond b]) with ((s ++ [Cond b]) ++ []) in H0 + by (rewrite app_nil_r; reflexivity). + replace (((s ++ [Cond b]) ++ []) ++ x) with ((s ++ [Cond b]) ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant (s ++ [Cond b]) [] x _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace (s ++ [Cond <{~b}>]) with ((s ++ [Cond <{~b}>]) ++ []) in H0 + by (rewrite app_nil_r; reflexivity). + replace (((s ++ [Cond <{~b}>]) ++ []) ++ x) with ((s ++ [Cond <{~b}>]) ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant (s ++ [Cond <{~b}>]) [] x _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace t with (t ++ []) in H0 + by (rewrite <- app_nil_r; reflexivity). + replace ((t ++ []) ++ x) with (t ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant _ _ _ _ _ H0). + + destruct (trace_extends _ _ _ _ H0); subst. + exists x. split. + * reflexivity. + * replace t with (t ++ []) in H0 + by (rewrite <- app_nil_r; reflexivity). + replace ((t ++ []) ++ x) with (t ++ x) in H0 + by (rewrite app_nil_r; reflexivity). + apply (prefix_irrelevant _ _ _ _ _ H0). +Qed. + +Lemma sequence_splits: forall p q t s, + (s, <{p ; q}>) ->* (t, SSkip) -> + exists t', + (s, p) ->* (t', SSkip) + /\ (t', q) ->* (t, SSkip). +Proof. + intros. apply clos_rtn1_rt1n in H. dependent induction H. destruct y. + apply clos_rt1n_rtn1 in H0. inversion H; subst. + - exists t0. split. + + constructor. + + apply H0. + - destruct (sequence_splits_step _ _ _ _ _ _ H H0) as (t' & ? & ?); subst. + destruct (IHclos_refl_trans_1n p' q (t0 ++ t') t0 eq_refl eq_refl) as (t'' & ? & ?). + exists t''. split. + + apply clos_rt1n_rtn1. econstructor. + * apply H2. + * apply clos_rtn1_rt1n. apply H1. + + apply H4. +Qed. + +(* and 5ii *) +Lemma sequence_concat: forall u p q, + canonical <{p ; q}> u -> + exists s t, u = s ++ t /\ canonical p s /\ canonical q t. +Proof. + intros. apply sequence_splits in H. + destruct H as (t' & ? & ?). + destruct (trace_extends _ _ _ _ H0); subst. + exists t'. exists x. repeat split. + + apply H. + + apply (prefix_irrelevant t'). rewrite app_nil_r. apply H0. +Qed. + +Require Import Wellfounded. +Require Import Psatz. +Lemma canonical_loop_end: forall b p t, + canonical <{while b {p}}> t -> + exists t', t = t' ++ [Cond <{ ~ b }>]. +Proof. + induction t using (well_founded_induction + (wf_inverse_image _ nat _ (@length _) + PeanoNat.Nat.lt_wf_0)); intros. + apply clos_rtn1_rt1n in H0. inversion H0; subst. inversion H1; subst. + - apply clos_rt1n_rtn1 in H2. simpl in H2. + destruct (trace_extends _ _ _ _ H2) as (t' & ->). + apply prefix_irrelevant_cons in H2. + destruct (sequence_concat _ _ _ H2) as (s & t & -> & ? & ?). + apply H in H4. destruct H4; subst. + exists ([Cond b] ++ s ++ x). + simpl. rewrite <- app_assoc. auto. + (* the list length *) + rewrite 2 app_length. simpl. lia. + - apply clos_rt1n_rtn1 in H2. + destruct (skip_non_productive _ _ _ H2) as [-> _]. + exists []. auto. +Qed. + +Definition indexed (A:Type):Type := nat -> A. + +(* this does build the trace "backwards", (b . sm . b . s(m-1) ... b . s0) but it's waaay easier to work with *) +Fixpoint build_loop_trace (b:Bexpr) (m:nat) (ts: indexed (list trace_step)): list trace_step := + match m with + | 0 => [] + | S n => [Cond b] ++ ts n ++ build_loop_trace b n ts + end. + +Lemma build_loop_ts_extentionally_eq: forall b m ts ts', + (forall n, n < m -> ts n = ts' n) -> build_loop_trace b m ts = build_loop_trace b m ts'. +Proof. + induction m; intros; auto. + simpl. rewrite (H m), (IHm _ ts'). reflexivity. + - intros. rewrite H; auto. + - auto. +Qed. + +(* surely this is somewhere in the standard library? *) +Fact lt_not_eqb: forall n m, n < m -> Nat.eqb n m = false. +Proof. + intros. destruct (eqb_spec n m). + - apply PeanoNat.Nat.lt_neq in H. contradiction. + - apply PeanoNat.Nat.eqb_neq; assumption. +Qed. + +Lemma canonical_loop: forall b p t, + canonical <{while b {p}}> t -> + exists m ts, t = build_loop_trace b m ts ++ [Cond <{~ b}>] + /\ forall i, i < m -> canonical p (ts i). +Proof. + induction t using (well_founded_induction + (wf_inverse_image _ nat _ (@length _) + PeanoNat.Nat.lt_wf_0)); intros. + apply clos_rtn1_rt1n in H0. inversion H0; subst. inversion H1; subst. + - apply clos_rt1n_rtn1 in H2. simpl in H2. + destruct (trace_extends _ _ _ _ H2) as (t' & ->). + apply prefix_irrelevant_cons in H2. + destruct (sequence_concat _ _ _ H2) as (s & t & -> & ? & ?). + apply H in H4. destruct H4 as (m & ts & -> & ?). + set (ts' := fun n => if Nat.eqb n m then s else ts n). + assert (Hts: ts' m = s) by (subst ts'; simpl; rewrite PeanoNat.Nat.eqb_refl; auto). + exists (S m). exists ts'. split. + + simpl. rewrite Hts. + replace (build_loop_trace b m ts') with (build_loop_trace b m ts). + rewrite app_assoc. auto. + assert (ts_ext_eq: forall i, i < m -> ts i = ts' i). { + intros. subst ts'; cbn. rewrite (lt_not_eqb _ _ H5). auto. + } + apply build_loop_ts_extentionally_eq; assumption. + + intros. apply Arith_prebase.lt_n_Sm_le in H5. + destruct (Lt.le_lt_or_eq_stt _ _ H5). + * subst ts'; cbn. rewrite (lt_not_eqb _ _ H6). apply H4; assumption. + * subst ts'; cbn. subst. rewrite PeanoNat.Nat.eqb_refl; assumption. + (* the list length stuff *) + + rewrite 2 app_length. simpl. lia. + - apply clos_rt1n_rtn1 in H2. + destruct (skip_non_productive _ _ _ H2) as [-> _]. + exists 0. exists (fun _ => []). split. + + auto. + + lia. +Qed. + +Lemma loop_canonical: forall b p m (ts: indexed (list trace_step)), + (forall i, i < m -> canonical p (ts i)) -> + canonical <{while b {p}}> (build_loop_trace b m ts ++ [Cond <{~ b}>]). +Proof. + induction m; intros. + - econstructor. + + apply (red_loop_false []). + + constructor. + - assert (H': forall i, i < m -> canonical p (ts i)) + by (intros; apply H; lia). + specialize (IHm ts H'). + apply clos_rt1n_rtn1. econstructor. + + apply red_loop_true. + + simpl. apply clos_rtn1_rt1n. + transitivity ([Cond b] ++ (ts m), <{skip ; while b {p}}>). + * apply sequence_star. apply canonical_extends. apply H. auto. + * apply clos_rt1n_rtn1. econstructor. + -- apply red_skip. + -- apply clos_rtn1_rt1n. + replace (Cond b :: (ts m ++ build_loop_trace b m ts) ++ [Cond <{ ~ b }>]) + with (([Cond b] ++ ts m) ++ (build_loop_trace b m ts) ++ [Cond <{ ~ b }>]) + by (simpl; rewrite app_assoc; auto). + apply canonical_extends; assumption. +Qed. diff --git a/Syntax.v b/Syntax.v new file mode 100644 index 0000000..796bee4 --- /dev/null +++ b/Syntax.v @@ -0,0 +1,47 @@ +From Coq Require Import Strings.String. +From BigStepSymbEx Require Import Expr. + +Module While. + Inductive Stmt : Type := + | SSkip + | SAsgn (x:string) (e:Aexpr) + | SSeq (s1 s2:Stmt) + | SIf (b:Bexpr) (s1 s2:Stmt) + | SWhile (b:Bexpr) (s:Stmt). + + Notation "'skip'" := SSkip (in custom com at level 80) : com_scope. + Notation "x := y" := + (SAsgn x y) + (in custom com at level 0, x constr at level 0, + y at level 85, no associativity) : com_scope. + Notation "x ; y" := + (SSeq x y) + (in custom com at level 90, right associativity) : com_scope. + Notation "'if' x '{' y '}' '{' z '}'" := + (SIf x y z) + (in custom com at level 89, x at level 99, + y at level 99, z at level 99) : com_scope. + Notation "'while' x '{' y '}'" := + (SWhile x y) + (in custom com at level 89, x at level 99, + y at level 99) : com_scope. + + Open Scope com_scope. + + Lemma seq_discriminate1: forall p q, p <> <{p ; q}>. + Proof. intros p q contra. induction p; + try discriminate. + inversion contra; subst. apply IHp1; assumption. + Qed. + + Lemma seq_discriminate2: forall p q, q <> <{p ; q}>. + Proof. intros p q contra. induction q; + try discriminate. + inversion contra; subst. apply IHq2; assumption. + Qed. + + Definition X: string := "x". + Definition Y: string := "y". + Definition Z: string := "z". + +End While. diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..95a2890 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,11 @@ +-R . BigStepSymbEx + +Limits.v +Expr.v +Maps.v + +Syntax.v +BigStep.v +SmallStep.v +Direct.v +Correspondence.v