From cd83285feccad4137e6bcaf9e8ce9db075fe73e2 Mon Sep 17 00:00:00 2001 From: Aqissiaq Date: Thu, 29 Jun 2023 17:55:11 +0200 Subject: [PATCH] Cleaned up for submission --- BigStep.v | 646 +++++++++++++++++++++++++++++++ BigStepExamples.v | 107 ++++++ Correspondence.v | 446 ++++++++++++++++++++++ Direct.v | 190 +++++++++ Expr.v | 30 ++ Limits.v | 73 ++++ Makefile | 953 ++++++++++++++++++++++++++++++++++++++++++++++ Makefile.conf | 64 ++++ Maps.v | 184 +++++++++ README.md | 29 +- SmallStep.v | 578 ++++++++++++++++++++++++++++ Syntax.v | 47 +++ _CoqProject | 11 + 13 files changed, 3356 insertions(+), 2 deletions(-) create mode 100644 BigStep.v create mode 100644 BigStepExamples.v create mode 100644 Correspondence.v create mode 100644 Direct.v create mode 100644 Expr.v create mode 100644 Limits.v create mode 100644 Makefile create mode 100644 Makefile.conf create mode 100644 Maps.v create mode 100644 SmallStep.v create mode 100644 Syntax.v create mode 100644 _CoqProject 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