From 62a83c575885d0b784d1ab585f8e3a6fbc5f3f79 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 7 Mar 2018 18:48:19 -0500 Subject: cpsloops --- src/Experiments/Loops.v | 381 +++++++++++++++++++++++++++++------------------- 1 file changed, 227 insertions(+), 154 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 94e127764..193fda390 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -3,44 +3,243 @@ Require Import Lia. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Option. Require Import Crypto.Util.Sum. Require Import Crypto.Util.LetIn. -Require Crypto.Util.ListUtil. (* for tests *) + +Require Import Crypto.Util.CPSNotations. Section Loops. - Context {continue_state break_state} - (body : continue_state -> break_state + continue_state) - (body_cps : continue_state -> - forall {T}, (break_state + continue_state -> T) - -> T). + Context {A B : Type} (body : A -> A + B). + + Definition loop (fuel : nat) (s : A) : A + B := + nat_rect _ (inl s) + (fun _ s => + match s with + | inl a => body a + | inr b => s + end + ) fuel. + + Context (body_cps : A ~> A + B). +(* WHY does the following not work? +Set Printing Universes. +Check (nat_rect (fun _ => forall R, (A+B -> R)->R) + (fun R ret => ret (inl s)) + (fun _ recurse => + recurse (forall R, (A + B -> R) -> R) + (fun s R ret => + match s with + | inl a => + s' <- body_cps a; + ret s' + | inr b => ret (inr b) + end + )) + fuel). +The term + "recurse (~> A + B) + (fun (s : A + B) (R : Type@{Top.1376}) (ret : A + B -> R) => + match s with + | inl a => s' <- body_cps a; + ret s' + | inr b => ret (inr b) + end)" has type "forall (R : Type@{Top.1376}) (_ : forall _ : sum A B, R), R" +while it is expected to have type + "forall (R : Type@{Top.1374}) (_ : forall _ : sum A B, R), R" +(universe inconsistency: Cannot enforce Top.1374 <= Top.1376 because Top.1376 +< Top.1375 <= Top.1374). *) + Definition loop_cps (fuel : nat) (s : A) : ~> A+B := + nat_rect (fun _ => forall R, (A + B -> R) -> R) + (fun R ret => ret (inl s)) + (fun _ recurse R => + recurse ((A + B -> R) -> R) + (fun s ret => + match s with + | inl a => + s' <- body_cps a; + ret s' + | inr b => ret (inr b) + end + )) fuel. + + Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). + Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). + Proof. + revert f; revert R; revert s; induction n; [reflexivity|]. + simpl loop; simpl loop_cps; intros. (* FIXME: unsimpl *) + rewrite IHn; break_match; [|reflexivity]. + cbv [cpscall]; rewrite body_cps_ok; reflexivity. + Qed. + + Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). + Definition loop_cps2 (fuel : nat) (s : A) : + forall {R} (timeout : A -> R) (ret : B -> R), R := + nat_rect (fun _ => forall R, (A -> R) -> (B -> R) -> R) + (fun R continue break => continue s) + (fun _ recurse R continue break => + recurse R (fun a => body_cps2 a R continue break) break + ) + fuel. + + Context (body_cps2_ok : forall s {R} continue break, + body_cps2 s R continue break = + match body s with + | inl a => continue a + | inr b => break b + end). + Lemma loop_cps2_ok n s {R} timeout ret : + @loop_cps2 n s R timeout ret = + match loop n s with + | inl a => timeout a + | inr b => ret b + end. + Proof. + revert ret; revert timeout; revert R; revert s; induction n; + [intros; reflexivity|]. + simpl loop; simpl loop_cps2; intros. (* FIXME: unsimpl *) + repeat (rewrite IHn || rewrite body_cps2_ok || break_match || congruence). + Qed. + + Lemma loop_fuel_0 s : loop 0 s = inl s. + Proof. reflexivity. Qed. + + Lemma loop_fuel_S n s : loop (S n) s = + match loop n s with + | inl a => body a + | inr b => loop n s + end. + Proof. reflexivity. Qed. + + Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. + Proof. + revert H; revert b; revert s; induction n; intros ? ? H. + { cbn [loop nat_rect] in H. congruence_sum. } + { rewrite loop_fuel_S. + break_match; congruence_sum; reflexivity. } + Qed. - Definition funapp {A B} (f : A -> B) (x : A) := f x. + Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. + Proof. + induction m; intros. + { rewrite PeanoNat.Nat.add_0_l. assumption. } + { rewrite PeanoNat.Nat.add_succ_l. + erewrite loop_fuel_S_stable; eauto. } + Qed. + + Lemma loop_fuel_irrelevant n m s bn bm + (Hn : loop n s = inr bn) + (Hm : loop m s = inr bm) + : bn = bm. + Proof. + destruct (Compare_dec.le_le_S_dec n m) as [H|H]; + destruct (PeanoNat.Nat.le_exists_sub _ _ H) as [d [? _]]; subst. + { erewrite loop_fuel_add_stable in Hm by eassumption; congruence. } + { erewrite loop_fuel_add_stable in Hn. + { congruence_sum. reflexivity. } + { erewrite loop_fuel_S_stable by eassumption. congruence. } } + Qed. + + Lemma by_invariant_with_inv_for_measure' (inv P:_->Prop) measure f s0 + (inv_init : inv s0) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_break : forall s s', body s = inr s' -> inv s -> P s') + (measure_decreases : forall s s', body s = inl s' -> inv s -> measure s' < measure s) + (measure_fuel : measure s0 < f) + : match loop f s0 with + | inl a => inv a + | inr s => P s + end. + Proof. + revert dependent s0; induction f; intros. + { exfalso; lia. } + Abort. (* I don't know how to prove this one *) + + Lemma by_invariant' P inv f s0 + (inv_init : inv s0) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_break : forall s s', body s = inr s' -> inv s -> P s') + : match loop f s0 with + | inl a => inv a + | inr s => P s + end. + Proof. + induction f. + { rewrite loop_fuel_0; auto. } + { rewrite loop_fuel_S. + destruct (loop f s0) eqn:Hn; + [ destruct (body a) eqn:Ha; eauto | eauto ]. } + Qed. + + Lemma by_invariant P inv f s0 b (H : loop f s0 = inr b) + (inv_init : inv s0) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_break : forall s s', body s = inr s' -> inv s -> P s') + : P b. + Proof. + pose proof (by_invariant' P inv f s0) as HH. + rewrite H in HH; eauto. + Qed. + + Lemma invariant_complete (P:_->Prop) f s0 b (Hf : loop f s0 = inr b) (H : P b) : + exists (inv : A -> Prop), + inv s0 + /\ (forall s s', body s = inl s' -> inv s -> inv s') + /\ (forall s s', body s = inr s' -> inv s -> P s'). + Proof. + exists (fun s => exists n, match loop n s0 with + | inl a => a = s + | _ => False end). + repeat split. + { exists 0. rewrite loop_fuel_0. reflexivity. } + { intros s s' Hss' [n Hn]. exists (S n). + destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. + rewrite loop_fuel_S, Hn, Hss'. reflexivity. } + { intros s s' Hss' [n Hn]. + destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. + assert (loop (S n) s0 = inr s') as HH by + (rewrite loop_fuel_S, Hn, Hss'; reflexivity). + rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hf); assumption. } + Qed. - Fixpoint loop_cps (fuel: nat) (start : continue_state) - {T} (ret : break_state -> T) : continue_state + T := - funapp - (body_cps start _) (fun next => - match next with - | inl state => inr (ret state) - | inr state => - match fuel with - | O => inl state - | S fuel' => - loop_cps fuel' state ret - end end). + Lemma loop_invariant_iff P f s0 b (H : loop f s0 = inr b) : + P b <-> + (exists (inv : A -> Prop), + inv s0 + /\ (forall s s', body s = inl s' -> inv s -> inv s') + /\ (forall s s', body s = inr s' -> inv s -> P s')). + Proof. + split. + { intros; eapply invariant_complete; eauto. } + { intros [? [?[]]]; eapply by_invariant; eauto. } + Qed. + + (* +WIP WIP - Fixpoint loop (fuel: nat) (start : continue_state) - : continue_state + break_state := - match (body start) with - | inl state => inr state - | inr state => - match fuel with - | O => inl state - | S fuel' => loop fuel' state + Fixpoint loop' (fuel : nat) (s : A) {struct fuel} : A + B := + match fuel with + | O => inl s + | S fuel' => + match body s with + | inl s => loop' fuel' s + | inr b => inr b end end. + + Fixpoint loop'_cps (fuel : nat) (s : A) {struct fuel} : ~> A + B := + match fuel with + | O => return (inl s) + | S fuel' => + s_b <- body_cps s; + match s_b with + | inl s => loop'_cps fuel' s + | inr b => return (inr b) + end + end. + Lemma loop_break_step fuel start state : (body start = inl state) -> @@ -89,33 +288,6 @@ Section Loops. Proof. cbv [terminates loop_default sum_rect] in *; break_match; congruence. Qed. - - Lemma invariant_iff fuel start default (H : terminates fuel start) P : - P (loop_default fuel start default) <-> - (exists (inv : continue_state -> Prop), - inv start - /\ (forall s s', body s = inr s' -> inv s -> inv s') - /\ (forall s s', body s = inl s' -> inv s -> P s')). - Proof. - split; - [ exists (fun st => exists f e, (loop f st = inr e /\ P e )) - | destruct 1 as [?[??]]; revert dependent start; induction fuel ]; - repeat match goal with - | _ => solve [ trivial | congruence | eauto ] - | _ => progress destruct_head' @ex - | _ => progress destruct_head' @and - | _ => progress intros - | _ => progress cbv [loop_default terminates] in * - | _ => progress cbn [loop] in * - | _ => progress erewrite loop_default_eq by eassumption - | _ => progress erewrite loop_continue_step in * by eassumption - | _ => progress erewrite loop_break_step in * by eassumption - | _ => progress break_match_hyps - | _ => progress break_match - | _ => progress eexists - | H1:_, c:_ |- _ => progress specialize (H1 c); congruence - end. - Qed. End Loops. Definition by_invariant {continue_state break_state body fuel start default} @@ -182,103 +354,4 @@ Definition for2 {state} (test : state -> bool) (increment body : state -> state) Definition for3 {state} init test increment body fuel := @for2 state test increment body fuel init. - -Module _test. - Section GCD. - Definition gcd_step := - fun '(a, b) => if Nat.ltb a b - then inr (a, b-a) - else if Nat.ltb b a - then inr (a-b, b) - else inl a. - - Definition gcd fuel a b := loop_default gcd_step fuel (a,b) 0. - - (* Eval cbv [gcd loop_default loop gcd_step] in (gcd 10 5 7). *) - - Example gcd_test : gcd 1000 28 35 = 7 := eq_refl. - - Definition gcd_step_cps - : (nat * nat) -> forall T, (nat + (nat * nat) -> T) -> T - := - fun st T ret => - let a := fst st in - let b := snd st in - if Nat.ltb a b - then ret (inr (a, b-a)) - else if Nat.ltb b a - then ret (inr (a-b, b)) - else ret (inl a). - - Definition gcd_cps fuel a b {T} (ret:nat->T) - := loop_cps gcd_step_cps fuel (a,b) ret. - - Example gcd_test2 : gcd_cps 1000 28 35 id = inr 7 := eq_refl. - - (* Eval cbv [gcd_cps loop_cps gcd_step_cps id] in (gcd_cps 2 5 7 id). *) - - End GCD. - - (* simple example--set all elements in a list to 0 *) - Section ZeroLoop. - Import Crypto.Util.ListUtil. - - Definition zero_body (state : nat * list nat) : - list nat + (nat * list nat) := - if dec (fst state < length (snd state)) - then inr (S (fst state), set_nth (fst state) 0 (snd state)) - else inl (snd state). - - Lemma zero_body_progress (arr : list nat) : - progress zero_body (fun state : nat * list nat => length (snd state) - fst state). - Proof. - cbv [zero_body progress]; intros until 0; - repeat match goal with - | _ => progress autorewrite with cancel_pair distr_length - | _ => progress subst - | _ => progress break_match; intros - | _ => congruence - | H: inl _ = inl _ |- _ => injection H; intros; subst; clear H - | H: inr _ = inr _ |- _ => injection H; intros; subst ;clear H - | _ => lia - end. - Qed. - - Definition zero_loop (arr : list nat) : list nat := - loop_default zero_body (length arr) (0,arr) nil. - - Definition zero_invariant (state : nat * list nat) := - fst state <= length (snd state) - /\ forall n, n < fst state -> nth_default 0 (snd state) n = 0. - - Lemma zero_correct (arr : list nat) : - forall n, nth_default 0 (zero_loop arr) n = 0. - Proof. - intros. cbv [zero_loop]. - eapply (by_invariant zero_invariant); eauto using zero_body_progress; - [ cbv [zero_invariant]; autorewrite with cancel_pair; split; intros; lia | ..]; - cbv [zero_invariant zero_body]; - intros until 0; - break_match; intros; - repeat match goal with - | _ => congruence - | H: inl _ = inl _ |- _ => injection H; intros; subst; clear H - | H: inr _ = inr _ |- _ => injection H; intros; subst ;clear H - | _ => progress split - | _ => progress intros - | _ => progress subst - | _ => progress (autorewrite with cancel_pair distr_length in * ) - | _ => rewrite set_nth_nth_default by lia - | _ => progress break_match - | H : _ /\ _ |- _ => destruct H - | H : (_,_) = ?x |- _ => - destruct x; inversion H; subst; destruct H - | H : _ |- _ => apply H; lia - | _ => lia - end. - destruct (Compare_dec.lt_dec n (fst s)). - apply H1; lia. - apply nth_default_out_of_bounds; lia. - Qed. - End ZeroLoop. -End _test. \ No newline at end of file +*) \ No newline at end of file -- cgit v1.2.3 From 911a397159a44426382995ae9d661cde45243649 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 8 Mar 2018 13:18:06 -0500 Subject: loops: more lemmas --- src/Experiments/Loops.v | 63 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 52 insertions(+), 11 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 193fda390..bd5341e5a 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -12,6 +12,17 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.CPSNotations. +(* TODO: do we have these anywhere? +Ltac forward H := + match type of H with + | ?A -> ?B => let HA := fresh in assert A as HA; [|specialize(H HA)] + end. +Ltac forward_by H t := + match type of H with + | ?A -> ?B => let HA := fresh in assert A as HA by t; [|specialize(H HA)] + end. + *) + Section Loops. Context {A B : Type} (body : A -> A + B). @@ -107,18 +118,30 @@ while it is expected to have type Lemma loop_fuel_0 s : loop 0 s = inl s. Proof. reflexivity. Qed. - Lemma loop_fuel_S n s : loop (S n) s = + Lemma loop_fuel_S_last n s : loop (S n) s = match loop n s with | inl a => body a | inr b => loop n s end. Proof. reflexivity. Qed. + Lemma loop_fuel_S_first n s : loop (S n) s = + match body s with + | inl a => loop n a + | inr b => inr b + end. + Proof. + revert s; induction n; intros s. + { break_match; rewrite ?loop_fuel_S_last, ?loop_fuel_0; congruence. } + { rewrite loop_fuel_S_last, IHn. + destruct (body s) eqn:?; [rewrite loop_fuel_S_last; reflexivity | reflexivity]. } + Qed. + Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. Proof. revert H; revert b; revert s; induction n; intros ? ? H. { cbn [loop nat_rect] in H. congruence_sum. } - { rewrite loop_fuel_S. + { rewrite loop_fuel_S_last. break_match; congruence_sum; reflexivity. } Qed. @@ -150,15 +173,33 @@ while it is expected to have type (measure_decreases : forall s s', body s = inl s' -> inv s -> measure s' < measure s) (measure_fuel : measure s0 < f) : match loop f s0 with - | inl a => inv a + | inl a => False | inr s => P s end. Proof. revert dependent s0; induction f; intros. { exfalso; lia. } - Abort. (* I don't know how to prove this one *) + { rewrite loop_fuel_S_first. + destruct (body s0) eqn:Hs0a; [|solve [eauto] ]. + specialize (IHf a). + specialize (inv_continue s0 a Hs0a inv_init). + specialize (measure_decreases s0 a). + specialize_by (assumption || lia); auto. } + Qed. + + Lemma by_invariant (inv P:_->Prop) measure f s0 + (inv_init : inv s0) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_break : forall s s', body s = inr s' -> inv s -> P s') + (measure_decreases : forall s s', body s = inl s' -> inv s -> measure s' < measure s) + (measure_fuel : measure s0 < f) + : exists b, loop f s0 = inr b /\ P b. + Proof. + pose proof (by_invariant_with_inv_for_measure' inv P measure f s0); + specialize_by assumption; break_match_hyps; [contradiction|eauto]. + Qed. - Lemma by_invariant' P inv f s0 + Lemma partial_by_invariant' P inv f s0 (inv_init : inv s0) (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') (inv_break : forall s s', body s = inr s' -> inv s -> P s') @@ -169,18 +210,18 @@ while it is expected to have type Proof. induction f. { rewrite loop_fuel_0; auto. } - { rewrite loop_fuel_S. + { rewrite loop_fuel_S_last. destruct (loop f s0) eqn:Hn; [ destruct (body a) eqn:Ha; eauto | eauto ]. } Qed. - Lemma by_invariant P inv f s0 b (H : loop f s0 = inr b) + Lemma partial_by_invariant P inv f s0 b (H : loop f s0 = inr b) (inv_init : inv s0) (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') (inv_break : forall s s', body s = inr s' -> inv s -> P s') : P b. Proof. - pose proof (by_invariant' P inv f s0) as HH. + pose proof (partial_by_invariant' P inv f s0) as HH. rewrite H in HH; eauto. Qed. @@ -197,11 +238,11 @@ while it is expected to have type { exists 0. rewrite loop_fuel_0. reflexivity. } { intros s s' Hss' [n Hn]. exists (S n). destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. - rewrite loop_fuel_S, Hn, Hss'. reflexivity. } + rewrite loop_fuel_S_last, Hn, Hss'. reflexivity. } { intros s s' Hss' [n Hn]. destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. assert (loop (S n) s0 = inr s') as HH by - (rewrite loop_fuel_S, Hn, Hss'; reflexivity). + (rewrite loop_fuel_S_last, Hn, Hss'; reflexivity). rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hf); assumption. } Qed. @@ -214,7 +255,7 @@ while it is expected to have type Proof. split. { intros; eapply invariant_complete; eauto. } - { intros [? [?[]]]; eapply by_invariant; eauto. } + { intros [? [?[]]]; eapply partial_by_invariant; eauto. } Qed. (* -- cgit v1.2.3 From 96b83fb67695305fcb1d286277c3a716a1c018e3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 8 Mar 2018 15:34:02 -0500 Subject: work on completeness of measure analysis --- src/Experiments/Loops.v | 113 ++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 104 insertions(+), 9 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index bd5341e5a..4a1ba3d88 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -166,7 +166,7 @@ while it is expected to have type { erewrite loop_fuel_S_stable by eassumption. congruence. } } Qed. - Lemma by_invariant_with_inv_for_measure' (inv P:_->Prop) measure f s0 + Lemma by_invariant' (inv P:_->Prop) measure f s0 (inv_init : inv s0) (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') (inv_break : forall s s', body s = inr s' -> inv s -> P s') @@ -195,11 +195,106 @@ while it is expected to have type (measure_fuel : measure s0 < f) : exists b, loop f s0 = inr b /\ P b. Proof. - pose proof (by_invariant_with_inv_for_measure' inv P measure f s0); + pose proof (by_invariant' inv P measure f s0); specialize_by assumption; break_match_hyps; [contradiction|eauto]. Qed. - Lemma partial_by_invariant' P inv f s0 + Definition iterations_required fuel s : option nat := + nat_rect _ None + (fun n r => + match r with + | Some _ => r + | None => + match loop (S n) s with + | inl a => None + | inr b => Some (S n) + end + end + ) fuel. + + Definition universal_measure f s := + match iterations_required f s with + | None => 0 + | Some s => pred s + end. + + Lemma iterations_required_sufficient fuel s n + (H:iterations_required fuel s = Some n) + : exists b, loop n s = inr b. + Proof. + induction fuel; [cbv in H; inversion H|]. + change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop (S fuel) s with + | inl _ => None + | inr _ => Some (S fuel) + end + | Some _ => iterations_required fuel s + end) in *. + destruct (iterations_required fuel s) eqn:?; inversion_option; [ solve[eauto] |]. + destruct (loop (S fuel) s) eqn:HH; inversion_option; []; subst. + rewrite HH; eauto. + Qed. + + Lemma iterations_required_le_fuel fuel s n + (H:iterations_required fuel s = Some n) : n <= fuel. + Proof. + revert H; revert n; revert s; induction fuel; intros. + { cbv in H. inversion H. } + change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop (S fuel) s with + | inl _ => None + | inr _ => Some (S fuel) + end + | Some _ => iterations_required fuel s + end) in *. + destruct (iterations_required fuel s) eqn:HH; inversion_option; subst. + { specialize (IHfuel _ _ HH); lia. } + { destruct (loop (S fuel) s) eqn:?; inversion_option; []; lia. } + Qed. + + Lemma iterations_required_complete fuel s b (H:loop fuel s = inr b) : + exists n, iterations_required fuel s = Some n /\ loop n s = inr b. + Proof. + induction fuel. + { rewrite loop_fuel_0 in H; inversion H. } + { change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop (S fuel) s with + | inl _ => None + | inr _ => Some (S fuel) + end + | Some _ => iterations_required fuel s + end) in *. + rewrite (loop_fuel_S_last fuel s). + destruct (loop fuel s) eqn:Heqs. + { pose proof H as HH. + rewrite loop_fuel_S_last, Heqs in HH; rewrite HH. + destruct (iterations_required fuel s) eqn:HX; [|solve [eauto]]. + apply iterations_required_sufficient in HX; destruct HX as [x Hx]. + exists n. (* unique *) admit. } + { destruct IHfuel as [? [Hx1 Hx2]]. + admit. (* unique *) + rewrite Hx1; eauto. } + Qed. + + Lemma inveriant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) + : exists inv measure, + inv s0 + /\ (forall s s', body s = inl s' -> inv s -> inv s') + /\ (forall s s', body s = inr s' -> inv s -> P s') + /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) + /\ measure s0 < f. + Proof. + exists (fun s => match loop (S (universal_measure f s)) s0 with + | inl a => False + | inr r => r = b end). + exists (universal_measure f). + repeat split. + { rewrite loop_fuel_S_first; break_match. + + Lemma partial_by_invariant P inv f s0 (inv_init : inv s0) (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') (inv_break : forall s s', body s = inr s' -> inv s -> P s') @@ -215,17 +310,17 @@ while it is expected to have type [ destruct (body a) eqn:Ha; eauto | eauto ]. } Qed. - Lemma partial_by_invariant P inv f s0 b (H : loop f s0 = inr b) + Lemma by_invariant_inr P inv f s0 b (H : loop f s0 = inr b) (inv_init : inv s0) (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') (inv_break : forall s s', body s = inr s' -> inv s -> P s') : P b. Proof. - pose proof (partial_by_invariant' P inv f s0) as HH. + pose proof (partial_by_invariant P inv f s0) as HH. rewrite H in HH; eauto. Qed. - Lemma invariant_complete (P:_->Prop) f s0 b (Hf : loop f s0 = inr b) (H : P b) : + Lemma by_invariant_inr_complete (P:_->Prop) f s0 b (Hf : loop f s0 = inr b) (H : P b) : exists (inv : A -> Prop), inv s0 /\ (forall s s', body s = inl s' -> inv s -> inv s') @@ -246,7 +341,7 @@ while it is expected to have type rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hf); assumption. } Qed. - Lemma loop_invariant_iff P f s0 b (H : loop f s0 = inr b) : + Lemma invariant_inr_iff P f s0 b (H : loop f s0 = inr b) : P b <-> (exists (inv : A -> Prop), inv s0 @@ -254,8 +349,8 @@ while it is expected to have type /\ (forall s s', body s = inr s' -> inv s -> P s')). Proof. split. - { intros; eapply invariant_complete; eauto. } - { intros [? [?[]]]; eapply partial_by_invariant; eauto. } + { intros; eapply by_invariant_inr_complete; eauto. } + { intros [? [?[]]]; eapply by_invariant_inr; eauto. } Qed. (* -- cgit v1.2.3 From b0e16bf803e601886fc8f8fcf4427ddd6592b5b7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 8 Mar 2018 23:18:32 -0500 Subject: wip completeness proof --- src/Experiments/Loops.v | 98 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 84 insertions(+), 14 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 4a1ba3d88..b331bc3f9 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -211,16 +211,10 @@ while it is expected to have type end end ) fuel. - - Definition universal_measure f s := - match iterations_required f s with - | None => 0 - | Some s => pred s - end. Lemma iterations_required_sufficient fuel s n (H:iterations_required fuel s = Some n) - : exists b, loop n s = inr b. + : exists b, loop n s = inr b /\ n <> 0. Proof. induction fuel; [cbv in H; inversion H|]. change (iterations_required (S fuel) s) @@ -237,7 +231,7 @@ while it is expected to have type Qed. Lemma iterations_required_le_fuel fuel s n - (H:iterations_required fuel s = Some n) : n <= fuel. + (H:iterations_required fuel s = Some n) : 1 <= n <= fuel. Proof. revert H; revert n; revert s; induction fuel; intros. { cbv in H. inversion H. } @@ -254,6 +248,34 @@ while it is expected to have type { destruct (loop (S fuel) s) eqn:?; inversion_option; []; lia. } Qed. + Lemma iterations_required_tight fuel s (H : iterations_required fuel s = None) + : forall n b, n <= fuel -> loop n s <> inr b. + Proof. + induction fuel; intros. + { replace n with 0 by lia. cbn. congruence. } + { change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop (S fuel) s with + | inl _ => None + | inr _ => Some (S fuel) + end + | Some _ => iterations_required fuel s + end) in *. + destruct (iterations_required fuel s) eqn:Hp; [inversion H|]. + specialize (IHfuel eq_refl n b). + destruct (Compare_dec.le_le_S_dec n fuel); [solve [eauto]|]. + replace n with (S fuel) in * by lia. + destruct (loop (S fuel) s); congruence. } + Qed. + + Lemma iterations_required_step fuel s s' n n' + (Hs : iterations_required (S fuel) s = Some n) + (Hs': iterations_required fuel s' = Some n') + (Hstep : body s = inl s') + : n = S n'. + Proof. + Admitted. + Lemma iterations_required_complete fuel s b (H:loop fuel s = inr b) : exists n, iterations_required fuel s = Some n /\ loop n s = inr b. Proof. @@ -272,13 +294,47 @@ while it is expected to have type { pose proof H as HH. rewrite loop_fuel_S_last, Heqs in HH; rewrite HH. destruct (iterations_required fuel s) eqn:HX; [|solve [eauto]]. - apply iterations_required_sufficient in HX; destruct HX as [x Hx]. - exists n. (* unique *) admit. } + apply iterations_required_sufficient in HX; destruct HX as [x [Hx _]]. + rewrite <-(loop_fuel_irrelevant _ _ _ _ _ Hx H); eauto. } { destruct IHfuel as [? [Hx1 Hx2]]. - admit. (* unique *) - rewrite Hx1; eauto. } + { rewrite <-(loop_fuel_irrelevant _ _ _ _ _ Heqs H); eauto. } + { rewrite Hx1; eauto. } } } Qed. + Definition universal_measure f s := + match iterations_required f s with + | None => 0 + | Some s => pred s + end. + + Lemma universal_measure_complete fuel s b (H:loop fuel s = inr b) : + loop (S (universal_measure fuel s)) s = inr b. + Proof. + cbv [universal_measure]. + destruct (iterations_required fuel s) as [n|] eqn:Heqn. + { destruct (iterations_required_sufficient fuel s _ Heqn) as [c [Hc Hnz]]. + rewrite PeanoNat.Nat.succ_pred by assumption. + rewrite (loop_fuel_irrelevant _ _ _ _ _ H Hc); assumption. } + { destruct(iterations_required_complete _ _ _ H) as [n [Hn _]]; + congruence. } + Qed. + + Lemma universal_measure_lt_fuel f s b (H:loop f s = inr b) : universal_measure f s < f. + Proof. + cbv [universal_measure]. + destruct (iterations_required f s) as [n|] eqn:Hn. + { pose proof iterations_required_le_fuel f s _ Hn; lia. } + { destruct (iterations_required_complete f s b H) as [?[]]; congruence. } + Qed. + + Lemma universal_measure_step fuel b s s' + (Hs : loop (S (universal_measure fuel s)) s = inr b) + (Hs': loop (universal_measure fuel s) s' = inr b) + (Hstep : body s = inl s') + : universal_measure fuel s = S (universal_measure fuel s'). + Proof. + Admitted. + Lemma inveriant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) : exists inv measure, inv s0 @@ -287,12 +343,26 @@ while it is expected to have type /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) /\ measure s0 < f. Proof. - exists (fun s => match loop (S (universal_measure f s)) s0 with + exists (fun s => match loop (S (universal_measure f s)) s with | inl a => False | inr r => r = b end). exists (universal_measure f). repeat split. - { rewrite loop_fuel_S_first; break_match. + { rewrite (universal_measure_complete _ _ _ H); reflexivity. } + { intros s s' Hstep Hinv. + destruct (loop (S (universal_measure f s)) s) eqn:Hs; [contradiction|subst]. + pose proof Hs as Hss. + rewrite loop_fuel_S_first, Hstep in Hs. + rewrite <-(universal_measure_step _ _ _ _ Hss Hs Hstep), Hs; reflexivity. } + { intros s c Hstep Hinv. + rewrite loop_fuel_S_first, Hstep in Hinv; congruence. } + { intros s s' Hstep Hinv. + destruct (loop (S (universal_measure f s)) s) eqn:Hf; [contradiction|]. + pose proof Hf as Hff. + rewrite loop_fuel_S_first, Hstep in Hf. + rewrite (universal_measure_step _ _ _ _ Hff Hf Hstep); lia. } + { exact (universal_measure_lt_fuel f s0 b H). } + Qed. Lemma partial_by_invariant P inv f s0 (inv_init : inv s0) -- cgit v1.2.3 From 0e4e1965dbc05b06e6a4a517cb7eb60c05e2ee4d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 14:28:51 -0400 Subject: prove iff --- src/Experiments/Loops.v | 219 ++++++++++++++++++++++-------------------------- 1 file changed, 98 insertions(+), 121 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index b331bc3f9..34d45fb3a 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -199,6 +199,8 @@ while it is expected to have type specialize_by assumption; break_match_hyps; [contradiction|eauto]. Qed. + (* Completeness proof *) + Definition iterations_required fuel s : option nat := nat_rect _ None (fun n r => @@ -211,48 +213,17 @@ while it is expected to have type end end ) fuel. - - Lemma iterations_required_sufficient fuel s n - (H:iterations_required fuel s = Some n) - : exists b, loop n s = inr b /\ n <> 0. - Proof. - induction fuel; [cbv in H; inversion H|]. - change (iterations_required (S fuel) s) - with (match iterations_required fuel s with - | None => match loop (S fuel) s with - | inl _ => None - | inr _ => Some (S fuel) - end - | Some _ => iterations_required fuel s - end) in *. - destruct (iterations_required fuel s) eqn:?; inversion_option; [ solve[eauto] |]. - destruct (loop (S fuel) s) eqn:HH; inversion_option; []; subst. - rewrite HH; eauto. - Qed. - Lemma iterations_required_le_fuel fuel s n - (H:iterations_required fuel s = Some n) : 1 <= n <= fuel. - Proof. - revert H; revert n; revert s; induction fuel; intros. - { cbv in H. inversion H. } - change (iterations_required (S fuel) s) - with (match iterations_required fuel s with - | None => match loop (S fuel) s with - | inl _ => None - | inr _ => Some (S fuel) - end - | Some _ => iterations_required fuel s - end) in *. - destruct (iterations_required fuel s) eqn:HH; inversion_option; subst. - { specialize (IHfuel _ _ HH); lia. } - { destruct (loop (S fuel) s) eqn:?; inversion_option; []; lia. } - Qed. - - Lemma iterations_required_tight fuel s (H : iterations_required fuel s = None) - : forall n b, n <= fuel -> loop n s <> inr b. + Lemma iterations_required_correct fuel s : + (forall m, iterations_required fuel s = Some m -> + 1 <= m <= fuel /\ + exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) + /\ + (iterations_required fuel s = None -> forall n, n <= fuel -> exists a, loop n s = inl a). Proof. induction fuel; intros. - { replace n with 0 by lia. cbn. congruence. } + { cbn. split; intros; inversion_option. + replace n with 0 by lia. rewrite loop_fuel_0. eauto. } { change (iterations_required (S fuel) s) with (match iterations_required fuel s with | None => match loop (S fuel) s with @@ -261,81 +232,46 @@ while it is expected to have type end | Some _ => iterations_required fuel s end) in *. - destruct (iterations_required fuel s) eqn:Hp; [inversion H|]. - specialize (IHfuel eq_refl n b). - destruct (Compare_dec.le_le_S_dec n fuel); [solve [eauto]|]. - replace n with (S fuel) in * by lia. - destruct (loop (S fuel) s); congruence. } + destruct (iterations_required fuel s) in *. + { split; intros; inversion_option; subst. + destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } + { destruct (loop (S fuel) s) eqn:HSf; split; intros; inversion_option; subst. + { intros. destruct (PeanoNat.Nat.eq_dec n (S fuel)); subst; eauto; []. + assert (n <= fuel) by lia. eapply IHfuel; congruence. } + { split; [lia|]. + exists b; intros; split; intros. + { eapply IHfuel; congruence || lia. } + { eapply PeanoNat.Nat.le_exists_sub in H; destruct H as [?[]]; subst. + eauto using loop_fuel_add_stable. } } } } Qed. - - Lemma iterations_required_step fuel s s' n n' - (Hs : iterations_required (S fuel) s = Some n) - (Hs': iterations_required fuel s' = Some n') - (Hstep : body s = inl s') - : n = S n'. - Proof. - Admitted. - Lemma iterations_required_complete fuel s b (H:loop fuel s = inr b) : - exists n, iterations_required fuel s = Some n /\ loop n s = inr b. - Proof. - induction fuel. - { rewrite loop_fuel_0 in H; inversion H. } - { change (iterations_required (S fuel) s) - with (match iterations_required fuel s with - | None => match loop (S fuel) s with - | inl _ => None - | inr _ => Some (S fuel) - end - | Some _ => iterations_required fuel s - end) in *. - rewrite (loop_fuel_S_last fuel s). - destruct (loop fuel s) eqn:Heqs. - { pose proof H as HH. - rewrite loop_fuel_S_last, Heqs in HH; rewrite HH. - destruct (iterations_required fuel s) eqn:HX; [|solve [eauto]]. - apply iterations_required_sufficient in HX; destruct HX as [x [Hx _]]. - rewrite <-(loop_fuel_irrelevant _ _ _ _ _ Hx H); eauto. } - { destruct IHfuel as [? [Hx1 Hx2]]. - { rewrite <-(loop_fuel_irrelevant _ _ _ _ _ Heqs H); eauto. } - { rewrite Hx1; eauto. } } } - Qed. - - Definition universal_measure f s := - match iterations_required f s with - | None => 0 - | Some s => pred s - end. - - Lemma universal_measure_complete fuel s b (H:loop fuel s = inr b) : - loop (S (universal_measure fuel s)) s = inr b. - Proof. - cbv [universal_measure]. - destruct (iterations_required fuel s) as [n|] eqn:Heqn. - { destruct (iterations_required_sufficient fuel s _ Heqn) as [c [Hc Hnz]]. - rewrite PeanoNat.Nat.succ_pred by assumption. - rewrite (loop_fuel_irrelevant _ _ _ _ _ H Hc); assumption. } - { destruct(iterations_required_complete _ _ _ H) as [n [Hn _]]; - congruence. } - Qed. - - Lemma universal_measure_lt_fuel f s b (H:loop f s = inr b) : universal_measure f s < f. - Proof. - cbv [universal_measure]. - destruct (iterations_required f s) as [n|] eqn:Hn. - { pose proof iterations_required_le_fuel f s _ Hn; lia. } - { destruct (iterations_required_complete f s b H) as [?[]]; congruence. } - Qed. - - Lemma universal_measure_step fuel b s s' - (Hs : loop (S (universal_measure fuel s)) s = inr b) - (Hs': loop (universal_measure fuel s) s' = inr b) + Lemma iterations_required_step fuel s s' n + (Hs : iterations_required fuel s = Some n) (Hstep : body s = inl s') - : universal_measure fuel s = S (universal_measure fuel s'). + : exists n', iterations_required fuel s' = Some n' /\ n = S n'. Proof. - Admitted. + eapply iterations_required_correct in Hs. + destruct Hs as [Hn [b Hs]]. + destruct n as [|n]; [pose proof (proj2 (Hs 0) ltac:(lia)) as Hx; inversion Hx|]. + exists n; split; [|reflexivity]. + pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. + rewrite loop_fuel_S_first, Hstep in H. + destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. + { eapply iterations_required_correct in Hs'; destruct Hs' as [Hx Hs']. + destruct Hs' as [b' Hs']. + destruct (Compare_dec.le_lt_dec n x) as [Hc|Hc]. + { destruct (Compare_dec.le_lt_dec x n) as [Hc'|Hc']; try lia; []. + destruct (proj1 (Hs' n) Hc'); congruence. } + { destruct (proj1 (Hs (S x)) ltac:(lia)) as [? HX]. + rewrite loop_fuel_S_first, Hstep in HX. + pose proof (proj2 (Hs' x) ltac:(lia)). + congruence. } } + { eapply iterations_required_correct in Hs'; [|exact (ltac:(lia) : n <= fuel)]. + destruct Hs'. + congruence. } + Qed. - Lemma inveriant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) + Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) : exists inv measure, inv s0 /\ (forall s s', body s = inl s' -> inv s -> inv s') @@ -343,25 +279,66 @@ while it is expected to have type /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) /\ measure s0 < f. Proof. - exists (fun s => match loop (S (universal_measure f s)) s with + set (measure f s := + match iterations_required f s with + | None => 0 + | Some s => pred s + end). + exists (fun s => match loop (S (measure f s)) s with | inl a => False | inr r => r = b end). - exists (universal_measure f). + exists (measure f). repeat split. - { rewrite (universal_measure_complete _ _ _ H); reflexivity. } + { cbv [measure]. + destruct (iterations_required f s0) eqn:Hs0; [|exfalso]. + { eapply iterations_required_correct in Hs0. + destruct Hs0 as [? [? Hs0]]. + replace (S (Nat.pred n)) with n by lia. + pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH. + exact (loop_fuel_irrelevant _ _ _ _ _ HH H). } + { eapply iterations_required_correct in Hs0; [|reflexivity]. + destruct_head'_ex; congruence. } } { intros s s' Hstep Hinv. - destruct (loop (S (universal_measure f s)) s) eqn:Hs; [contradiction|subst]. - pose proof Hs as Hss. + destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. + cbv [measure] in *. + destruct (iterations_required f s) eqn:Hs' in *; [|cbv in Hs; congruence]. + destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. + rewrite HA. + destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]]. + pose proof (HE' ltac:(constructor)) as HE; clear HE'. + replace (S (Nat.pred (S x))) with (S x) in * by lia. rewrite loop_fuel_S_first, Hstep in Hs. - rewrite <-(universal_measure_step _ _ _ _ Hss Hs Hstep), Hs; reflexivity. } + replace (S (Nat.pred x)) with x in * by lia; rewrite HE. + exact (loop_fuel_irrelevant _ _ _ _ _ HE Hs). } { intros s c Hstep Hinv. - rewrite loop_fuel_S_first, Hstep in Hinv; congruence. } + destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. + change (loop 1 s = inr c) in Hstep. + rewrite (loop_fuel_irrelevant _ _ _ _ _ Hstep Hs); exact HP. } { intros s s' Hstep Hinv. - destruct (loop (S (universal_measure f s)) s) eqn:Hf; [contradiction|]. - pose proof Hf as Hff. - rewrite loop_fuel_S_first, Hstep in Hf. - rewrite (universal_measure_step _ _ _ _ Hff Hf Hstep); lia. } - { exact (universal_measure_lt_fuel f s0 b H). } + destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. + cbv [measure] in *. + destruct (iterations_required f s) eqn:Hs' in *; [|cbv in Hs; congruence]. + destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. + rewrite HA. + apply iterations_required_correct in HA; lia. } + { cbv [measure]. + destruct (iterations_required f s0 ) eqn:Hs; + eapply iterations_required_correct in Hs; [lia| | exact (ltac:(lia): f <= f) ]. + destruct_head'_ex; congruence. } + Qed. + + Lemma invariant_iff f s0 P : + (exists b, loop f s0 = inr b /\ P b) + <-> + (exists inv measure, + inv s0 + /\ (forall s s', body s = inl s' -> inv s -> inv s') + /\ (forall s s', body s = inr s' -> inv s -> P s') + /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) + /\ measure s0 < f). + Proof. + repeat (intros || split || destruct_head'_ex || destruct_head'_and); + eauto using invariant_complete, by_invariant. Qed. Lemma partial_by_invariant P inv f s0 -- cgit v1.2.3 From d95956e526f06c9c132804c088c988cbbe634951 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 14:39:18 -0400 Subject: refactor measure --- src/Experiments/Loops.v | 65 +++++++++++++++++-------------------------------- 1 file changed, 22 insertions(+), 43 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 34d45fb3a..07e6d2b68 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -167,32 +167,27 @@ while it is expected to have type Qed. Lemma by_invariant' (inv P:_->Prop) measure f s0 - (inv_init : inv s0) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_init : inv s0 /\ measure s0 < f) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) (inv_break : forall s s', body s = inr s' -> inv s -> P s') - (measure_decreases : forall s s', body s = inl s' -> inv s -> measure s' < measure s) - (measure_fuel : measure s0 < f) : match loop f s0 with | inl a => False | inr s => P s end. Proof. - revert dependent s0; induction f; intros. + revert dependent s0; induction f; intros; destruct_head'_and. { exfalso; lia. } { rewrite loop_fuel_S_first. destruct (body s0) eqn:Hs0a; [|solve [eauto] ]. specialize (IHf a). - specialize (inv_continue s0 a Hs0a inv_init). - specialize (measure_decreases s0 a). - specialize_by (assumption || lia); auto. } + destruct (inv_continue s0 a Hs0a ltac:(assumption)). + specialize_by (split; (auto || lia)); auto. } Qed. Lemma by_invariant (inv P:_->Prop) measure f s0 - (inv_init : inv s0) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') + (inv_init : inv s0 /\ measure s0 < f) + (inv_continue : forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) (inv_break : forall s s', body s = inr s' -> inv s -> P s') - (measure_decreases : forall s s', body s = inl s' -> inv s -> measure s' < measure s) - (measure_fuel : measure s0 < f) : exists b, loop f s0 = inr b /\ P b. Proof. pose proof (by_invariant' inv P measure f s0); @@ -273,11 +268,9 @@ while it is expected to have type Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) : exists inv measure, - inv s0 - /\ (forall s s', body s = inl s' -> inv s -> inv s') - /\ (forall s s', body s = inr s' -> inv s -> P s') - /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) - /\ measure s0 < f. + (inv s0 /\ measure s0 < f) + /\ (forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) + /\ (forall s s', body s = inr s' -> inv s -> P s'). Proof. set (measure f s := match iterations_required f s with @@ -287,17 +280,15 @@ while it is expected to have type exists (fun s => match loop (S (measure f s)) s with | inl a => False | inr r => r = b end). - exists (measure f). - repeat split. + exists (measure f); split; [ |repeat match goal with |- _ /\ _ => split end..]. { cbv [measure]. - destruct (iterations_required f s0) eqn:Hs0; [|exfalso]. - { eapply iterations_required_correct in Hs0. - destruct Hs0 as [? [? Hs0]]. - replace (S (Nat.pred n)) with n by lia. - pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH. - exact (loop_fuel_irrelevant _ _ _ _ _ HH H). } - { eapply iterations_required_correct in Hs0; [|reflexivity]. - destruct_head'_ex; congruence. } } + destruct (iterations_required f s0) eqn:Hs0; + eapply iterations_required_correct in Hs0; + [ .. | exact (ltac:(lia):f <= f)]; [|destruct_head'_ex; congruence]. + destruct Hs0 as [? [? Hs0]]. + replace (S (Nat.pred n)) with n by lia. + pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH. + split; [exact (loop_fuel_irrelevant _ _ _ _ _ HH H) | lia]. } { intros s s' Hstep Hinv. destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. cbv [measure] in *. @@ -306,6 +297,7 @@ while it is expected to have type rewrite HA. destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]]. pose proof (HE' ltac:(constructor)) as HE; clear HE'. + split; [|lia]. replace (S (Nat.pred (S x))) with (S x) in * by lia. rewrite loop_fuel_S_first, Hstep in Hs. replace (S (Nat.pred x)) with x in * by lia; rewrite HE. @@ -314,28 +306,15 @@ while it is expected to have type destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. change (loop 1 s = inr c) in Hstep. rewrite (loop_fuel_irrelevant _ _ _ _ _ Hstep Hs); exact HP. } - { intros s s' Hstep Hinv. - destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. - cbv [measure] in *. - destruct (iterations_required f s) eqn:Hs' in *; [|cbv in Hs; congruence]. - destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. - rewrite HA. - apply iterations_required_correct in HA; lia. } - { cbv [measure]. - destruct (iterations_required f s0 ) eqn:Hs; - eapply iterations_required_correct in Hs; [lia| | exact (ltac:(lia): f <= f) ]. - destruct_head'_ex; congruence. } Qed. Lemma invariant_iff f s0 P : (exists b, loop f s0 = inr b /\ P b) <-> (exists inv measure, - inv s0 - /\ (forall s s', body s = inl s' -> inv s -> inv s') - /\ (forall s s', body s = inr s' -> inv s -> P s') - /\ (forall s s', body s = inl s' -> inv s -> measure s' < measure s) - /\ measure s0 < f). + (inv s0 /\ measure s0 < f) + /\ (forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) + /\ (forall s s', body s = inr s' -> inv s -> P s')). Proof. repeat (intros || split || destruct_head'_ex || destruct_head'_and); eauto using invariant_complete, by_invariant. -- cgit v1.2.3 From 9b17c18c0bac42fef5a1dd35097f58fab05ce9bd Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 16:39:34 -0400 Subject: tail recursion --- src/Experiments/Loops.v | 282 ++++++++++++++++-------------------------------- 1 file changed, 93 insertions(+), 189 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 07e6d2b68..fca28d737 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -26,75 +26,47 @@ Ltac forward_by H t := Section Loops. Context {A B : Type} (body : A -> A + B). - Definition loop (fuel : nat) (s : A) : A + B := - nat_rect _ (inl s) - (fun _ s => - match s with - | inl a => body a - | inr b => s - end - ) fuel. + Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := + match fuel with + | O => inl s + | S fuel' => + let s := body s in + match s with + | inl a => loop fuel' a + | inr b => inr b + end + end. Context (body_cps : A ~> A + B). -(* WHY does the following not work? -Set Printing Universes. -Check (nat_rect (fun _ => forall R, (A+B -> R)->R) - (fun R ret => ret (inl s)) - (fun _ recurse => - recurse (forall R, (A + B -> R) -> R) - (fun s R ret => - match s with - | inl a => - s' <- body_cps a; - ret s' - | inr b => ret (inr b) - end - )) - fuel). -The term - "recurse (~> A + B) - (fun (s : A + B) (R : Type@{Top.1376}) (ret : A + B -> R) => - match s with - | inl a => s' <- body_cps a; - ret s' - | inr b => ret (inr b) - end)" has type "forall (R : Type@{Top.1376}) (_ : forall _ : sum A B, R), R" -while it is expected to have type - "forall (R : Type@{Top.1374}) (_ : forall _ : sum A B, R), R" -(universe inconsistency: Cannot enforce Top.1374 <= Top.1376 because Top.1376 -< Top.1375 <= Top.1374). *) - Definition loop_cps (fuel : nat) (s : A) : ~> A+B := - nat_rect (fun _ => forall R, (A + B -> R) -> R) - (fun R ret => ret (inl s)) - (fun _ recurse R => - recurse ((A + B -> R) -> R) - (fun s ret => - match s with - | inl a => - s' <- body_cps a; - ret s' - | inr b => ret (inr b) - end - )) fuel. + + Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := + match fuel with + | O => return (inl s) + | S fuel' => + s <- body_cps s; + match s with + | inl a => loop_cps fuel' a + | inr b => return (inr b) + end + end. Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). Proof. - revert f; revert R; revert s; induction n; [reflexivity|]. - simpl loop; simpl loop_cps; intros. (* FIXME: unsimpl *) - rewrite IHn; break_match; [|reflexivity]. - cbv [cpscall]; rewrite body_cps_ok; reflexivity. + revert f; revert R; revert s; induction n; [reflexivity|]; cbn; intros. + cbv [cpscall cpsreturn]; rewrite body_cps_ok; + break_match; rewrite ?IHn; reflexivity. Qed. Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). - Definition loop_cps2 (fuel : nat) (s : A) : - forall {R} (timeout : A -> R) (ret : B -> R), R := - nat_rect (fun _ => forall R, (A -> R) -> (B -> R) -> R) - (fun R continue break => continue s) - (fun _ recurse R continue break => - recurse R (fun a => body_cps2 a R continue break) break - ) - fuel. + Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := + match fuel with + | O => timeout s + | S fuel' => + body_cps2 s R + (fun a => @loop_cps2 fuel' a R timeout ret) + (fun b => ret b) + end. Context (body_cps2_ok : forall s {R} continue break, body_cps2 s R continue break = @@ -102,39 +74,39 @@ while it is expected to have type | inl a => continue a | inr b => break b end). - Lemma loop_cps2_ok n s {R} timeout ret : + Lemma loop_cps2_ok n s {R} (timeout ret : _ -> R) : @loop_cps2 n s R timeout ret = match loop n s with | inl a => timeout a | inr b => ret b end. Proof. - revert ret; revert timeout; revert R; revert s; induction n; - [intros; reflexivity|]. - simpl loop; simpl loop_cps2; intros. (* FIXME: unsimpl *) - repeat (rewrite IHn || rewrite body_cps2_ok || break_match || congruence). + revert ret; revert timeout; revert R; revert s; + induction n; intros; cbn; [reflexivity|]. + rewrite body_cps2_ok. + destruct (body s); [|reflexivity]. + rewrite IHn. reflexivity. Qed. Lemma loop_fuel_0 s : loop 0 s = inl s. Proof. reflexivity. Qed. - Lemma loop_fuel_S_last n s : loop (S n) s = - match loop n s with - | inl a => body a - | inr b => loop n s - end. - Proof. reflexivity. Qed. - Lemma loop_fuel_S_first n s : loop (S n) s = match body s with | inl a => loop n a | inr b => inr b end. + Proof. reflexivity. Qed. + + Lemma loop_fuel_S_last n s : loop (S n) s = + match loop n s with + | inl a => body a + | inr b => loop n s + end. Proof. - revert s; induction n; intros s. - { break_match; rewrite ?loop_fuel_S_last, ?loop_fuel_0; congruence. } - { rewrite loop_fuel_S_last, IHn. - destruct (body s) eqn:?; [rewrite loop_fuel_S_last; reflexivity | reflexivity]. } + revert s; induction n; cbn; intros s. + { break_match; reflexivity. } + { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } Qed. Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. @@ -292,7 +264,8 @@ while it is expected to have type { intros s s' Hstep Hinv. destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. cbv [measure] in *. - destruct (iterations_required f s) eqn:Hs' in *; [|cbv in Hs; congruence]. + destruct (iterations_required f s) eqn:Hs' in *; + [|rewrite loop_fuel_S_last in Hs; cbv in Hs; congruence]. destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. rewrite HA. destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]]. @@ -304,8 +277,8 @@ while it is expected to have type exact (loop_fuel_irrelevant _ _ _ _ _ HE Hs). } { intros s c Hstep Hinv. destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. - change (loop 1 s = inr c) in Hstep. - rewrite (loop_fuel_irrelevant _ _ _ _ _ Hstep Hs); exact HP. } + assert (HH: loop 1 s = inr c) by (cbn; rewrite Hstep; reflexivity). + rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hs); exact HP. } Qed. Lemma invariant_iff f s0 P : @@ -378,132 +351,63 @@ while it is expected to have type { intros; eapply by_invariant_inr_complete; eauto. } { intros [? [?[]]]; eapply by_invariant_inr; eauto. } Qed. +End Loops. - (* -WIP WIP - - Fixpoint loop' (fuel : nat) (s : A) {struct fuel} : A + B := - match fuel with - | O => inl s - | S fuel' => - match body s with - | inl s => loop' fuel' s - | inr b => inr b - end end. - - Fixpoint loop'_cps (fuel : nat) (s : A) {struct fuel} : ~> A + B := - match fuel with - | O => return (inl s) - | S fuel' => - s_b <- body_cps s; - match s_b with - | inl s => loop'_cps fuel' s - | inr b => return (inr b) - end - end. - - - Lemma loop_break_step fuel start state : - (body start = inl state) -> - loop fuel start = inr state. - Proof. - destruct fuel; simpl loop; break_match; intros; congruence. - Qed. - - Lemma loop_continue_step fuel start state : - (body start = inr state) -> - loop fuel start = - match fuel with | O => inl state | S fuel' => loop fuel' state end. - Proof. - destruct fuel; simpl loop; break_match; intros; congruence. - Qed. - - (* TODO: provide [invariant state] to proofs of this *) - Definition progress (measure : continue_state -> nat) := - forall state state', body state = inr state' -> measure state' < measure state. - Definition terminates fuel start := forall l, loop fuel start <> inl l. - Lemma terminates_by_measure measure (H : progress measure) : - forall fuel start, measure start <= fuel -> terminates fuel start. - Proof. - induction fuel; intros; - repeat match goal with - | _ => solve [ congruence | lia ] - | _ => progress cbv [progress terminates] in * - | _ => progress cbn [loop] - | _ => progress break_match - | H : forall _ _, body _ = inr _ -> _ , Heq : body _ = inr _ |- _ => specialize (H _ _ Heq) - | _ => eapply IHfuel - end. - Qed. +Module silent. + Section Silent. + Context {state} (body : state -> state + state). + Definition loop fuel s : state := + match loop body fuel s with + | inl s => s + | inr s => s + end. - Definition loop_default fuel start default - : break_state := - sum_rect - (fun _ => break_state) - (fun _ => default) - (fun result => result) - (loop fuel start). - - Lemma loop_default_eq fuel start default - (Hterm : terminates fuel start) : - loop fuel start = inr (loop_default fuel start default). - Proof. - cbv [terminates loop_default sum_rect] in *; break_match; congruence. - Qed. -End Loops. + Lemma by_invariant inv (P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 < f) + (step : forall s s' : state, + body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) + (fini: forall s s' : state, body s = inr s' -> inv s -> P s') + : P (loop f s0). + Proof. + edestruct (by_invariant body inv P measure f s0) as [x [A B]]; eauto; []. + apply (f_equal (fun r : state + state => match r with inl s => s | inr s => s end)) in A. + cbv [loop]; break_match; congruence. + Qed. + End Silent. +End silent. -Definition by_invariant {continue_state break_state body fuel start default} - invariant measure P invariant_start invariant_continue invariant_break le_start progress - := proj2 (@invariant_iff continue_state break_state body fuel start default (terminates_by_measure body measure progress fuel start le_start) P) - (ex_intro _ invariant (conj invariant_start (conj invariant_continue invariant_break))). -Arguments terminates_by_measure {_ _ _}. - Module while. Section While. Context {state} (test : state -> bool) (body : state -> state). - Fixpoint while (fuel: nat) (s : state) {struct fuel} : state := - if test s - then - let s := body s in - match fuel with - | O => s - | S fuel' => while fuel' s - end - else s. + Fixpoint while f s := + match f with + | O => s + | S f => + if test s + then while f (body s) + else s + end. Section AsLoop. - Local Definition lbody := fun s => if test s then inr (body s) else inl s. + Local Definition lbody := fun s => if test s then inl (body s) else inr s. - Lemma eq_loop : forall fuel start, while fuel start = loop_default lbody fuel start (while fuel start). + Lemma eq_loop f s : while f s = sum_rect (fun _ => _) id id (loop lbody f s). Proof. - induction fuel; intros; - cbv [lbody loop_default sum_rect id] in *; - cbn [while loop]; [|rewrite IHfuel]; break_match; auto. + revert s; induction f; intros s; [reflexivity|]. + { cbv [lbody sum_rect id] in *; cbn in *. + rewrite IHf; break_innermost_match; reflexivity. } Qed. - Lemma by_invariant fuel start - (invariant : state -> Prop) (measure : state -> nat) (P : state -> Prop) - (_: invariant start) - (_: forall s, invariant s -> if test s then invariant (body s) else P s) - (_: measure start <= fuel) - (_: forall s, if test s then measure (body s) < measure s else True) - : P (while fuel start). + Lemma by_invariant inv P measure f s0 + (init : inv s0 /\ measure s0 < f) + (step : forall s, if test s + then inv s -> inv (body s) /\ measure (body s) < measure s + else P (body s)) + : P (while f s0). Proof. - rewrite eq_loop; cbv [lbody]. - eapply (by_invariant invariant measure); - repeat match goal with - | [ H : forall s, invariant s -> _, G: invariant ?s |- _ ] => unique pose proof (H _ G) - | [ H : forall s, if ?f s then _ else _, G: ?f ?s = _ |- _ ] => unique pose proof (H s) - | _ => solve [ trivial | congruence ] - | _ => progress cbv [progress] - | _ => progress intros - | _ => progress subst - | _ => progress inversion_sum - | _ => progress break_match_hyps (* FIXME: this must be last? *) - end. Qed. End AsLoop. End While. -- cgit v1.2.3 From 32e61a3682eb90c46714926487e70147eb734e31 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 17:01:41 -0400 Subject: comprehensive --- src/Experiments/Loops.v | 699 +++++++++++++++++++++++------------------------- 1 file changed, 341 insertions(+), 358 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index fca28d737..13bd6df2f 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -12,346 +12,308 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.CPSNotations. -(* TODO: do we have these anywhere? -Ltac forward H := - match type of H with - | ?A -> ?B => let HA := fresh in assert A as HA; [|specialize(H HA)] - end. -Ltac forward_by H t := - match type of H with - | ?A -> ?B => let HA := fresh in assert A as HA by t; [|specialize(H HA)] - end. - *) - -Section Loops. - Context {A B : Type} (body : A -> A + B). - - Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := - match fuel with - | O => inl s - | S fuel' => - let s := body s in - match s with - | inl a => loop fuel' a - | inr b => inr b - end - end. - - Context (body_cps : A ~> A + B). - - Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := - match fuel with - | O => return (inl s) - | S fuel' => - s <- body_cps s; +Module Import core. + Section Loops. + Context {A B : Type} (body : A -> A + B). + + Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := + match fuel with + | O => inl s + | S fuel' => + let s := body s in match s with - | inl a => loop_cps fuel' a - | inr b => return (inr b) + | inl a => loop fuel' a + | inr b => inr b end - end. - - Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). - Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). - Proof. - revert f; revert R; revert s; induction n; [reflexivity|]; cbn; intros. - cbv [cpscall cpsreturn]; rewrite body_cps_ok; - break_match; rewrite ?IHn; reflexivity. - Qed. - - Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). - Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := - match fuel with - | O => timeout s - | S fuel' => - body_cps2 s R - (fun a => @loop_cps2 fuel' a R timeout ret) - (fun b => ret b) - end. - - Context (body_cps2_ok : forall s {R} continue break, - body_cps2 s R continue break = - match body s with - | inl a => continue a - | inr b => break b - end). - Lemma loop_cps2_ok n s {R} (timeout ret : _ -> R) : - @loop_cps2 n s R timeout ret = - match loop n s with - | inl a => timeout a - | inr b => ret b - end. - Proof. - revert ret; revert timeout; revert R; revert s; - induction n; intros; cbn; [reflexivity|]. - rewrite body_cps2_ok. - destruct (body s); [|reflexivity]. - rewrite IHn. reflexivity. - Qed. - - Lemma loop_fuel_0 s : loop 0 s = inl s. - Proof. reflexivity. Qed. - - Lemma loop_fuel_S_first n s : loop (S n) s = - match body s with - | inl a => loop n a - | inr b => inr b - end. - Proof. reflexivity. Qed. - - Lemma loop_fuel_S_last n s : loop (S n) s = - match loop n s with - | inl a => body a - | inr b => loop n s - end. - Proof. - revert s; induction n; cbn; intros s. - { break_match; reflexivity. } - { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } - Qed. - - Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. - Proof. - revert H; revert b; revert s; induction n; intros ? ? H. - { cbn [loop nat_rect] in H. congruence_sum. } - { rewrite loop_fuel_S_last. - break_match; congruence_sum; reflexivity. } - Qed. - - Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. - Proof. - induction m; intros. - { rewrite PeanoNat.Nat.add_0_l. assumption. } - { rewrite PeanoNat.Nat.add_succ_l. - erewrite loop_fuel_S_stable; eauto. } - Qed. - - Lemma loop_fuel_irrelevant n m s bn bm - (Hn : loop n s = inr bn) - (Hm : loop m s = inr bm) - : bn = bm. - Proof. - destruct (Compare_dec.le_le_S_dec n m) as [H|H]; - destruct (PeanoNat.Nat.le_exists_sub _ _ H) as [d [? _]]; subst. - { erewrite loop_fuel_add_stable in Hm by eassumption; congruence. } - { erewrite loop_fuel_add_stable in Hn. - { congruence_sum. reflexivity. } - { erewrite loop_fuel_S_stable by eassumption. congruence. } } - Qed. - - Lemma by_invariant' (inv P:_->Prop) measure f s0 - (inv_init : inv s0 /\ measure s0 < f) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) - (inv_break : forall s s', body s = inr s' -> inv s -> P s') - : match loop f s0 with - | inl a => False - | inr s => P s end. - Proof. - revert dependent s0; induction f; intros; destruct_head'_and. - { exfalso; lia. } - { rewrite loop_fuel_S_first. - destruct (body s0) eqn:Hs0a; [|solve [eauto] ]. - specialize (IHf a). - destruct (inv_continue s0 a Hs0a ltac:(assumption)). - specialize_by (split; (auto || lia)); auto. } - Qed. - - Lemma by_invariant (inv P:_->Prop) measure f s0 - (inv_init : inv s0 /\ measure s0 < f) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) - (inv_break : forall s s', body s = inr s' -> inv s -> P s') - : exists b, loop f s0 = inr b /\ P b. - Proof. - pose proof (by_invariant' inv P measure f s0); - specialize_by assumption; break_match_hyps; [contradiction|eauto]. - Qed. - - (* Completeness proof *) - - Definition iterations_required fuel s : option nat := - nat_rect _ None - (fun n r => - match r with - | Some _ => r - | None => - match loop (S n) s with - | inl a => None - | inr b => Some (S n) + + Context (body_cps : A ~> A + B). + + Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := + match fuel with + | O => return (inl s) + | S fuel' => + s <- body_cps s; + match s with + | inl a => loop_cps fuel' a + | inr b => return (inr b) + end + end. + + Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). + Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). + Proof. + revert f; revert R; revert s; induction n; [reflexivity|]; cbn; intros. + cbv [cpscall cpsreturn]; rewrite body_cps_ok; + break_match; rewrite ?IHn; reflexivity. + Qed. + + Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). + Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := + match fuel with + | O => timeout s + | S fuel' => + body_cps2 s R + (fun a => @loop_cps2 fuel' a R timeout ret) + (fun b => ret b) + end. + + Context (body_cps2_ok : forall s {R} continue break, + body_cps2 s R continue break = + match body s with + | inl a => continue a + | inr b => break b + end). + Lemma loop_cps2_ok n s {R} (timeout ret : _ -> R) : + @loop_cps2 n s R timeout ret = + match loop n s with + | inl a => timeout a + | inr b => ret b + end. + Proof. + revert ret; revert timeout; revert R; revert s; + induction n; intros; cbn; [reflexivity|]. + rewrite body_cps2_ok. + destruct (body s); [|reflexivity]. + rewrite IHn. reflexivity. + Qed. + + Lemma loop_fuel_0 s : loop 0 s = inl s. + Proof. reflexivity. Qed. + + Lemma loop_fuel_S_first n s : loop (S n) s = + match body s with + | inl a => loop n a + | inr b => inr b + end. + Proof. reflexivity. Qed. + + Lemma loop_fuel_S_last n s : loop (S n) s = + match loop n s with + | inl a => body a + | inr b => loop n s + end. + Proof. + revert s; induction n; cbn; intros s. + { break_match; reflexivity. } + { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } + Qed. + + Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. + Proof. + revert H; revert b; revert s; induction n; intros ? ? H. + { cbn [loop nat_rect] in H. congruence_sum. } + { rewrite loop_fuel_S_last. + break_match; congruence_sum; reflexivity. } + Qed. + + Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. + Proof. + induction m; intros. + { rewrite PeanoNat.Nat.add_0_l. assumption. } + { rewrite PeanoNat.Nat.add_succ_l. + erewrite loop_fuel_S_stable; eauto. } + Qed. + + Lemma loop_fuel_irrelevant n m s bn bm + (Hn : loop n s = inr bn) + (Hm : loop m s = inr bm) + : bn = bm. + Proof. + destruct (Compare_dec.le_le_S_dec n m) as [H|H]; + destruct (PeanoNat.Nat.le_exists_sub _ _ H) as [d [? _]]; subst. + { erewrite loop_fuel_add_stable in Hm by eassumption; congruence. } + { erewrite loop_fuel_add_stable in Hn. + { congruence_sum. reflexivity. } + { erewrite loop_fuel_S_stable by eassumption. congruence. } } + Qed. + + Lemma by_invariant' (inv P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 < f) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : match loop f s0 with + | inl a => False + | inr s => P s + end. + Proof. + revert dependent s0; induction f; intros; destruct_head'_and. + { exfalso; lia. } + { rewrite loop_fuel_S_first. + specialize (step s0 H); destruct (body s0); [|assumption]. + destruct step. + exact (IHf a ltac:(split; (assumption || lia))). } + Qed. + + Lemma by_invariant (inv P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 < f) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : exists b, loop f s0 = inr b /\ P b. + Proof. + pose proof (by_invariant' inv P measure f s0); + specialize_by assumption; break_match_hyps; [contradiction|eauto]. + Qed. + + (* Completeness proof *) + + Definition iterations_required fuel s : option nat := + nat_rect _ None + (fun n r => + match r with + | Some _ => r + | None => + match loop (S n) s with + | inl a => None + | inr b => Some (S n) + end end - end - ) fuel. + ) fuel. - Lemma iterations_required_correct fuel s : - (forall m, iterations_required fuel s = Some m -> - 1 <= m <= fuel /\ - exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) + Lemma iterations_required_correct fuel s : + (forall m, iterations_required fuel s = Some m -> + 1 <= m <= fuel /\ + exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) /\ - (iterations_required fuel s = None -> forall n, n <= fuel -> exists a, loop n s = inl a). - Proof. - induction fuel; intros. - { cbn. split; intros; inversion_option. - replace n with 0 by lia. rewrite loop_fuel_0. eauto. } - { change (iterations_required (S fuel) s) - with (match iterations_required fuel s with - | None => match loop (S fuel) s with - | inl _ => None - | inr _ => Some (S fuel) - end - | Some _ => iterations_required fuel s - end) in *. - destruct (iterations_required fuel s) in *. - { split; intros; inversion_option; subst. - destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } - { destruct (loop (S fuel) s) eqn:HSf; split; intros; inversion_option; subst. - { intros. destruct (PeanoNat.Nat.eq_dec n (S fuel)); subst; eauto; []. - assert (n <= fuel) by lia. eapply IHfuel; congruence. } - { split; [lia|]. - exists b; intros; split; intros. - { eapply IHfuel; congruence || lia. } - { eapply PeanoNat.Nat.le_exists_sub in H; destruct H as [?[]]; subst. - eauto using loop_fuel_add_stable. } } } } - Qed. - - Lemma iterations_required_step fuel s s' n - (Hs : iterations_required fuel s = Some n) - (Hstep : body s = inl s') - : exists n', iterations_required fuel s' = Some n' /\ n = S n'. - Proof. - eapply iterations_required_correct in Hs. - destruct Hs as [Hn [b Hs]]. - destruct n as [|n]; [pose proof (proj2 (Hs 0) ltac:(lia)) as Hx; inversion Hx|]. - exists n; split; [|reflexivity]. - pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. - rewrite loop_fuel_S_first, Hstep in H. - destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. - { eapply iterations_required_correct in Hs'; destruct Hs' as [Hx Hs']. - destruct Hs' as [b' Hs']. - destruct (Compare_dec.le_lt_dec n x) as [Hc|Hc]. - { destruct (Compare_dec.le_lt_dec x n) as [Hc'|Hc']; try lia; []. - destruct (proj1 (Hs' n) Hc'); congruence. } - { destruct (proj1 (Hs (S x)) ltac:(lia)) as [? HX]. - rewrite loop_fuel_S_first, Hstep in HX. - pose proof (proj2 (Hs' x) ltac:(lia)). - congruence. } } - { eapply iterations_required_correct in Hs'; [|exact (ltac:(lia) : n <= fuel)]. - destruct Hs'. - congruence. } - Qed. - - Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) - : exists inv measure, - (inv s0 /\ measure s0 < f) - /\ (forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) - /\ (forall s s', body s = inr s' -> inv s -> P s'). - Proof. - set (measure f s := - match iterations_required f s with - | None => 0 - | Some s => pred s - end). - exists (fun s => match loop (S (measure f s)) s with - | inl a => False - | inr r => r = b end). - exists (measure f); split; [ |repeat match goal with |- _ /\ _ => split end..]. - { cbv [measure]. - destruct (iterations_required f s0) eqn:Hs0; - eapply iterations_required_correct in Hs0; - [ .. | exact (ltac:(lia):f <= f)]; [|destruct_head'_ex; congruence]. - destruct Hs0 as [? [? Hs0]]. - replace (S (Nat.pred n)) with n by lia. - pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH. - split; [exact (loop_fuel_irrelevant _ _ _ _ _ HH H) | lia]. } - { intros s s' Hstep Hinv. - destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. - cbv [measure] in *. - destruct (iterations_required f s) eqn:Hs' in *; - [|rewrite loop_fuel_S_last in Hs; cbv in Hs; congruence]. - destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. - rewrite HA. - destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]]. - pose proof (HE' ltac:(constructor)) as HE; clear HE'. - split; [|lia]. - replace (S (Nat.pred (S x))) with (S x) in * by lia. - rewrite loop_fuel_S_first, Hstep in Hs. - replace (S (Nat.pred x)) with x in * by lia; rewrite HE. - exact (loop_fuel_irrelevant _ _ _ _ _ HE Hs). } - { intros s c Hstep Hinv. - destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. - assert (HH: loop 1 s = inr c) by (cbn; rewrite Hstep; reflexivity). - rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hs); exact HP. } - Qed. - - Lemma invariant_iff f s0 P : - (exists b, loop f s0 = inr b /\ P b) - <-> - (exists inv measure, + (iterations_required fuel s = None -> forall n, n <= fuel -> exists a, loop n s = inl a). + Proof. + induction fuel; intros. + { cbn. split; intros; inversion_option. + replace n with 0 by lia. rewrite loop_fuel_0. eauto. } + { change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop (S fuel) s with + | inl _ => None + | inr _ => Some (S fuel) + end + | Some _ => iterations_required fuel s + end) in *. + destruct (iterations_required fuel s) in *. + { split; intros; inversion_option; subst. + destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } + { destruct (loop (S fuel) s) eqn:HSf; split; intros; inversion_option; subst. + { intros. destruct (PeanoNat.Nat.eq_dec n (S fuel)); subst; eauto; []. + assert (n <= fuel) by lia. eapply IHfuel; congruence. } + { split; [lia|]. + exists b; intros; split; intros. + { eapply IHfuel; congruence || lia. } + { eapply PeanoNat.Nat.le_exists_sub in H; destruct H as [?[]]; subst. + eauto using loop_fuel_add_stable. } } } } + Qed. + + Lemma iterations_required_step fuel s s' n + (Hs : iterations_required fuel s = Some n) + (Hstep : body s = inl s') + : exists n', iterations_required fuel s' = Some n' /\ n = S n'. + Proof. + eapply iterations_required_correct in Hs. + destruct Hs as [Hn [b Hs]]. + destruct n as [|n]; [pose proof (proj2 (Hs 0) ltac:(lia)) as Hx; inversion Hx|]. + exists n; split; [|reflexivity]. + pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. + rewrite loop_fuel_S_first, Hstep in H. + destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. + { eapply iterations_required_correct in Hs'; destruct Hs' as [Hx Hs']. + destruct Hs' as [b' Hs']. + destruct (Compare_dec.le_lt_dec n x) as [Hc|Hc]. + { destruct (Compare_dec.le_lt_dec x n) as [Hc'|Hc']; try lia; []. + destruct (proj1 (Hs' n) Hc'); congruence. } + { destruct (proj1 (Hs (S x)) ltac:(lia)) as [? HX]. + rewrite loop_fuel_S_first, Hstep in HX. + pose proof (proj2 (Hs' x) ltac:(lia)). + congruence. } } + { eapply iterations_required_correct in Hs'; [|exact (ltac:(lia) : n <= fuel)]. + destruct Hs'. + congruence. } + Qed. + + Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) + : exists inv measure, (inv s0 /\ measure s0 < f) - /\ (forall s s', body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) - /\ (forall s s', body s = inr s' -> inv s -> P s')). - Proof. - repeat (intros || split || destruct_head'_ex || destruct_head'_and); - eauto using invariant_complete, by_invariant. - Qed. - - Lemma partial_by_invariant P inv f s0 - (inv_init : inv s0) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') - (inv_break : forall s s', body s = inr s' -> inv s -> P s') - : match loop f s0 with - | inl a => inv a - | inr s => P s + /\ forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end. + Proof. + set (measure f s := + match iterations_required f s with + | None => 0 + | Some s => pred s + end). + exists (fun s => match loop (S (measure f s)) s with + | inl a => False + | inr r => r = b end). + exists (measure f); split; [ |repeat match goal with |- _ /\ _ => split end..]. + { cbv [measure]. + destruct (iterations_required f s0) eqn:Hs0; + eapply iterations_required_correct in Hs0; + [ .. | exact (ltac:(lia):f <= f)]; [|destruct_head'_ex; congruence]. + destruct Hs0 as [? [? Hs0]]. + replace (S (Nat.pred n)) with n by lia. + pose proof (proj2 (Hs0 n) ltac:(lia)) as HH; rewrite HH. + split; [exact (loop_fuel_irrelevant _ _ _ _ _ HH H) | lia]. } + { intros s Hinv; destruct (body s) as [s'|c] eqn:Hstep. + { destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. + cbv [measure] in *. + destruct (iterations_required f s) eqn:Hs' in *; + [|rewrite loop_fuel_S_last in Hs; cbv in Hs; congruence]. + destruct (iterations_required_step _ _ s' _ Hs' Hstep) as [? [HA ?]]; subst. + rewrite HA. + destruct (proj1 (iterations_required_correct _ _) _ HA) as [? [? [? HE']]]. + pose proof (HE' ltac:(constructor)) as HE; clear HE'. + split; [|lia]. + replace (S (Nat.pred (S x))) with (S x) in * by lia. + rewrite loop_fuel_S_first, Hstep in Hs. + replace (S (Nat.pred x)) with x in * by lia; rewrite HE. + exact (loop_fuel_irrelevant _ _ _ _ _ HE Hs). } + { destruct (loop (S (measure f s)) s) eqn:Hs; [contradiction|subst]. + assert (HH: loop 1 s = inr c) by (cbn; rewrite Hstep; reflexivity). + rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hs); exact HP. } } + Qed. + + Lemma invariant_iff f s0 P : + (exists b, loop f s0 = inr b /\ P b) + <-> + (exists inv measure, + (inv s0 /\ measure s0 < f) + /\ forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end). + Proof. + repeat (intros || split || destruct_head'_ex || destruct_head'_and); + eauto using invariant_complete, by_invariant. + Qed. + End Loops. +End core. + +Module default. + Section Default. + Context {A B} (default : B) (body : A -> A + B). + Definition loop fuel s : B := + match loop body fuel s with + | inl s => default + | inr s => s end. - Proof. - induction f. - { rewrite loop_fuel_0; auto. } - { rewrite loop_fuel_S_last. - destruct (loop f s0) eqn:Hn; - [ destruct (body a) eqn:Ha; eauto | eauto ]. } - Qed. - - Lemma by_invariant_inr P inv f s0 b (H : loop f s0 = inr b) - (inv_init : inv s0) - (inv_continue : forall s s', body s = inl s' -> inv s -> inv s') - (inv_break : forall s s', body s = inr s' -> inv s -> P s') - : P b. - Proof. - pose proof (partial_by_invariant P inv f s0) as HH. - rewrite H in HH; eauto. - Qed. - - Lemma by_invariant_inr_complete (P:_->Prop) f s0 b (Hf : loop f s0 = inr b) (H : P b) : - exists (inv : A -> Prop), - inv s0 - /\ (forall s s', body s = inl s' -> inv s -> inv s') - /\ (forall s s', body s = inr s' -> inv s -> P s'). - Proof. - exists (fun s => exists n, match loop n s0 with - | inl a => a = s - | _ => False end). - repeat split. - { exists 0. rewrite loop_fuel_0. reflexivity. } - { intros s s' Hss' [n Hn]. exists (S n). - destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. - rewrite loop_fuel_S_last, Hn, Hss'. reflexivity. } - { intros s s' Hss' [n Hn]. - destruct (loop n s0) eqn:Hn_; [|contradiction]; subst a; rename Hn_ into Hn. - assert (loop (S n) s0 = inr s') as HH by - (rewrite loop_fuel_S_last, Hn, Hss'; reflexivity). - rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hf); assumption. } - Qed. - - Lemma invariant_inr_iff P f s0 b (H : loop f s0 = inr b) : - P b <-> - (exists (inv : A -> Prop), - inv s0 - /\ (forall s s', body s = inl s' -> inv s -> inv s') - /\ (forall s s', body s = inr s' -> inv s -> P s')). - Proof. - split. - { intros; eapply by_invariant_inr_complete; eauto. } - { intros [? [?[]]]; eapply by_invariant_inr; eauto. } - Qed. -End Loops. + + Lemma by_invariant inv (P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 < f) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop f s0). + Proof. + edestruct (by_invariant body inv P measure f s0) as [x [HA HB]]; eauto; []. + apply (f_equal (fun r : A + B => match r with inl s => default | inr s => s end)) in HA. + cbv [loop]; break_match; congruence. + Qed. + End Default. +End default. Module silent. Section Silent. @@ -364,9 +326,10 @@ Module silent. Lemma by_invariant inv (P:_->Prop) measure f s0 (init : inv s0 /\ measure s0 < f) - (step : forall s s' : state, - body s = inl s' -> inv s -> inv s' /\ measure s' < measure s) - (fini: forall s s' : state, body s = inr s' -> inv s -> P s') + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) : P (loop f s0). Proof. edestruct (by_invariant body inv P measure f s0) as [x [A B]]; eauto; []. @@ -391,33 +354,53 @@ Module while. else s end. - Section AsLoop. - Local Definition lbody := fun s => if test s then inl (body s) else inr s. - - Lemma eq_loop f s : while f s = sum_rect (fun _ => _) id id (loop lbody f s). - Proof. - revert s; induction f; intros s; [reflexivity|]. - { cbv [lbody sum_rect id] in *; cbn in *. - rewrite IHf; break_innermost_match; reflexivity. } - Qed. - - Lemma by_invariant inv P measure f s0 - (init : inv s0 /\ measure s0 < f) - (step : forall s, if test s - then inv s -> inv (body s) /\ measure (body s) < measure s - else P (body s)) - : P (while f s0). - Proof. - Qed. - End AsLoop. + Local Definition lbody := fun s => if test s then inl (body s) else inr s. + + Lemma eq_loop f s : while f s = silent.loop lbody f s. + Proof. + revert s; induction f; intros s; [reflexivity|]. + cbn; cbv [silent.loop lbody] in *. + rewrite IHf. + cbn; cbv [silent.loop lbody]. + break_match; reflexivity. + Qed. + + Lemma by_invariant inv P measure f s0 + (init : inv s0 /\ measure s0 < f) + (step : forall s, inv s -> if test s + then inv (body s) /\ measure (body s) < measure s + else P s) + : P (while f s0). + Proof. + rewrite eq_loop. + eapply silent.by_invariant; eauto; []; intros s H; cbv [lbody]. + specialize (step s H); destruct (test s); eauto. + Qed. + + Context (body_cps : state ~> state). + + Fixpoint while_cps f s :~> state := + match f with + | O => return s + | S f => + if test s + then s <- body_cps s; while_cps f s + else return s + end. + + Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). + Lemma loop_cps_ok n s {R} f : while_cps n s R f = f (while n s). + Proof. + revert s; induction n; intros s; [reflexivity|]. + cbn; break_match; + cbv [cpscall cpsreturn]; rewrite ?body_cps_ok, ?IHn; reflexivity. + Qed. End While. - Arguments by_invariant {_ _ _ _ _}. End while. Notation while := while.while. Definition for2 {state} (test : state -> bool) (increment body : state -> state) - := while test (fun s => increment (body s)). + := while test (fun s => let s := body s in increment s). Definition for3 {state} init test increment body fuel := - @for2 state test increment body fuel init. -*) \ No newline at end of file + @for2 state test increment body fuel init. \ No newline at end of file -- cgit v1.2.3 From ff97b19808c081d3923573eaf69549a361b94195 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 18:07:23 -0400 Subject: cleanup --- src/Experiments/Loops.v | 286 +++++++++++++++++++++++++++++------------------- 1 file changed, 172 insertions(+), 114 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index 13bd6df2f..e5c8bf2ef 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -16,47 +16,60 @@ Module Import core. Section Loops. Context {A B : Type} (body : A -> A + B). + (* the fuel parameter is only present to allow defining a loop + without proving its termination. The loop body does not have + access to the amount of remaining fuel, and thus increasing fuel + beyond termination cannot change the behavior. fuel counts full + loops -- the one that exacutes "break" is not included *) + Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := - match fuel with - | O => inl s - | S fuel' => - let s := body s in - match s with - | inl a => loop fuel' a - | inr b => inr b - end + let s := body s in + match s with + | inl a => + match fuel with + | O => inl a + | S fuel' => loop fuel' a + end + | inr b => inr b end. Context (body_cps : A ~> A + B). Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := - match fuel with - | O => return (inl s) - | S fuel' => - s <- body_cps s; - match s with - | inl a => loop_cps fuel' a - | inr b => return (inr b) - end - end. + s <- body_cps s; + match s with + | inl a => + match fuel with + | O => return (inl a) + | S fuel' => loop_cps fuel' a + end + | inr b => return (inr b) + end. Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). Proof. - revert f; revert R; revert s; induction n; [reflexivity|]; cbn; intros. - cbv [cpscall cpsreturn]; rewrite body_cps_ok; - break_match; rewrite ?IHn; reflexivity. + revert f; revert R; revert s; induction n; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps_ok + | _ => progress rewrite ?IHn + | _ => progress break_match + | _ => reflexivity + end. Qed. Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := - match fuel with - | O => timeout s - | S fuel' => - body_cps2 s R - (fun a => @loop_cps2 fuel' a R timeout ret) - (fun b => ret b) - end. + body_cps2 s R + (fun a => + match fuel with + | O => timeout a + | S fuel' => @loop_cps2 fuel' a R timeout ret + end) + (fun b => ret b). Context (body_cps2_ok : forall s {R} continue break, body_cps2 s R continue break = @@ -71,15 +84,22 @@ Module Import core. | inr b => ret b end. Proof. - revert ret; revert timeout; revert R; revert s; - induction n; intros; cbn; [reflexivity|]. - rewrite body_cps2_ok. - destruct (body s); [|reflexivity]. - rewrite IHn. reflexivity. + revert timeout; revert ret; revert R; revert s; induction n; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps2_ok + | _ => progress rewrite ?IHn + | _ => progress inversion_sum + | _ => progress subst + | _ => progress break_match + | _ => reflexivity + end. Qed. - Lemma loop_fuel_0 s : loop 0 s = inl s. - Proof. reflexivity. Qed. + Lemma loop_fuel_0 s : loop 0 s = body s. + Proof. cbv; break_match; reflexivity. Qed. Lemma loop_fuel_S_first n s : loop (S n) s = match body s with @@ -102,7 +122,7 @@ Module Import core. Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. Proof. revert H; revert b; revert s; induction n; intros ? ? H. - { cbn [loop nat_rect] in H. congruence_sum. } + { cbn [loop nat_rect] in *; break_match_hyps; congruence_sum; congruence. } { rewrite loop_fuel_S_last. break_match; congruence_sum; reflexivity. } Qed. @@ -128,8 +148,8 @@ Module Import core. { erewrite loop_fuel_S_stable by eassumption. congruence. } } Qed. - Lemma by_invariant' (inv P:_->Prop) measure f s0 - (init : inv s0 /\ measure s0 < f) + Lemma by_invariant_fuel' (inv P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' @@ -140,25 +160,34 @@ Module Import core. end. Proof. revert dependent s0; induction f; intros; destruct_head'_and. - { exfalso; lia. } + { specialize (step s0 H); cbv; break_innermost_match; [lia|assumption]. } { rewrite loop_fuel_S_first. specialize (step s0 H); destruct (body s0); [|assumption]. destruct step. exact (IHf a ltac:(split; (assumption || lia))). } Qed. - Lemma by_invariant (inv P:_->Prop) measure f s0 - (init : inv s0 /\ measure s0 < f) + Lemma by_invariant_fuel (inv P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' end) : exists b, loop f s0 = inr b /\ P b. Proof. - pose proof (by_invariant' inv P measure f s0); + pose proof (by_invariant_fuel' inv P measure f s0); specialize_by assumption; break_match_hyps; [contradiction|eauto]. Qed. + Lemma by_invariant (inv P:_->Prop) measure s0 + (init : inv s0) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : exists b, loop (measure s0) s0 = inr b /\ P b. + Proof. eapply by_invariant_fuel; eauto. Qed. + (* Completeness proof *) Definition iterations_required fuel s : option nat := @@ -167,37 +196,36 @@ Module Import core. match r with | Some _ => r | None => - match loop (S n) s with + match loop n s with | inl a => None - | inr b => Some (S n) + | inr b => Some n end end ) fuel. Lemma iterations_required_correct fuel s : (forall m, iterations_required fuel s = Some m -> - 1 <= m <= fuel /\ + m < fuel /\ exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) /\ - (iterations_required fuel s = None -> forall n, n <= fuel -> exists a, loop n s = inl a). + (iterations_required fuel s = None -> forall n, n < fuel -> exists a, loop n s = inl a). Proof. induction fuel; intros. - { cbn. split; intros; inversion_option. - replace n with 0 by lia. rewrite loop_fuel_0. eauto. } + { cbn. split; intros; inversion_option; lia. } { change (iterations_required (S fuel) s) with (match iterations_required fuel s with - | None => match loop (S fuel) s with + | None => match loop fuel s with | inl _ => None - | inr _ => Some (S fuel) + | inr _ => Some fuel end | Some _ => iterations_required fuel s end) in *. destruct (iterations_required fuel s) in *. { split; intros; inversion_option; subst. destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } - { destruct (loop (S fuel) s) eqn:HSf; split; intros; inversion_option; subst. - { intros. destruct (PeanoNat.Nat.eq_dec n (S fuel)); subst; eauto; []. - assert (n <= fuel) by lia. eapply IHfuel; congruence. } + { destruct (loop fuel s) eqn:HSf; split; intros; inversion_option; subst. + { intros. destruct (PeanoNat.Nat.eq_dec n fuel); subst; eauto; []. + assert (n < fuel) by lia. eapply IHfuel; congruence. } { split; [lia|]. exists b; intros; split; intros. { eapply IHfuel; congruence || lia. } @@ -206,14 +234,12 @@ Module Import core. Qed. Lemma iterations_required_step fuel s s' n - (Hs : iterations_required fuel s = Some n) + (Hs : iterations_required fuel s = Some (S n)) (Hstep : body s = inl s') - : exists n', iterations_required fuel s' = Some n' /\ n = S n'. + : iterations_required fuel s' = Some n. Proof. eapply iterations_required_correct in Hs. destruct Hs as [Hn [b Hs]]. - destruct n as [|n]; [pose proof (proj2 (Hs 0) ltac:(lia)) as Hx; inversion Hx|]. - exists n; split; [|reflexivity]. pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. rewrite loop_fuel_S_first, Hstep in H. destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. @@ -226,67 +252,60 @@ Module Import core. rewrite loop_fuel_S_first, Hstep in HX. pose proof (proj2 (Hs' x) ltac:(lia)). congruence. } } - { eapply iterations_required_correct in Hs'; [|exact (ltac:(lia) : n <= fuel)]. - destruct Hs'. - congruence. } + { eapply iterations_required_correct in Hs'; destruct Hs' as [? Hs']; + [|exact Hn]. + rewrite loop_fuel_S_last, H in Hs'; congruence. } Qed. Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) : exists inv measure, - (inv s0 /\ measure s0 < f) + (inv s0 /\ measure s0 <= f) /\ forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' end. Proof. - set (measure f s := - match iterations_required f s with - | None => 0 - | Some s => pred s - end). - exists (fun s => match loop (S (measure f s)) s with + set (measure s := match iterations_required (S f) s with None => 0 | Some n => n end). + exists (fun s => match loop (measure s) s with | inl a => False | inr r => r = b end). - exists (measure f); split; [ |repeat match goal with |- _ /\ _ => split end..]. + exists (measure); split; [ |repeat match goal with |- _ /\ _ => split end..]. { cbv [measure]. - destruct (iterations_required f s0) eqn:Hs0; + destruct (iterations_required (S f) s0) eqn:Hs0; eapply iterations_required_correct in Hs0; - [ .. | exact (ltac:(lia):f <= f)]; [|destruct_head'_ex; congruence]. - destruct Hs0 as [? [? Hs0]]. - replace (S (Nat.pred n)) with n by lia. + [ .. | exact (ltac:(lia):f (exists inv measure, - (inv s0 /\ measure s0 < f) + (inv s0 /\ measure s0 <= f) /\ forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' end). Proof. repeat (intros || split || destruct_head'_ex || destruct_head'_and); - eauto using invariant_complete, by_invariant. + eauto using invariant_complete, by_invariant_fuel. Qed. End Loops. End core. @@ -300,18 +319,27 @@ Module default. | inr s => s end. - Lemma by_invariant inv (P:_->Prop) measure f s0 - (init : inv s0 /\ measure s0 < f) + Lemma by_invariant_fuel inv (P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 <= f) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' end) : P (loop f s0). Proof. - edestruct (by_invariant body inv P measure f s0) as [x [HA HB]]; eauto; []. + edestruct (by_invariant_fuel body inv P measure f s0) as [x [HA HB]]; eauto; []. apply (f_equal (fun r : A + B => match r with inl s => default | inr s => s end)) in HA. cbv [loop]; break_match; congruence. Qed. + + Lemma by_invariant (inv P:_->Prop) measure s0 + (init : inv s0) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. End Default. End default. @@ -324,18 +352,27 @@ Module silent. | inr s => s end. - Lemma by_invariant inv (P:_->Prop) measure f s0 - (init : inv s0 /\ measure s0 < f) + Lemma by_invariant_fuel inv (P:_->Prop) measure f s0 + (init : inv s0 /\ measure s0 <= f) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s | inr s' => P s' end) : P (loop f s0). Proof. - edestruct (by_invariant body inv P measure f s0) as [x [A B]]; eauto; []. + edestruct (by_invariant_fuel body inv P measure f s0) as [x [A B]]; eauto; []. apply (f_equal (fun r : state + state => match r with inl s => s | inr s => s end)) in A. cbv [loop]; break_match; congruence. Qed. + + Lemma by_invariant (inv P:_->Prop) measure s0 + (init : inv s0) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. End Silent. End silent. @@ -346,54 +383,75 @@ Module while. (body : state -> state). Fixpoint while f s := - match f with - | O => s - | S f => - if test s - then while f (body s) - else s - end. + if test s + then + let s := body s in + match f with + | O => s + | S f => while f s + end + else s. Local Definition lbody := fun s => if test s then inl (body s) else inr s. Lemma eq_loop f s : while f s = silent.loop lbody f s. Proof. - revert s; induction f; intros s; [reflexivity|]. - cbn; cbv [silent.loop lbody] in *. - rewrite IHf. - cbn; cbv [silent.loop lbody]. - break_match; reflexivity. + revert s; induction f; intros s; + repeat match goal with + | _ => progress cbn in * + | _ => progress cbv [silent.loop lbody] in * + | _ => rewrite IHf + | _ => progress break_match + | _ => congruence + end. Qed. - Lemma by_invariant inv P measure f s0 - (init : inv s0 /\ measure s0 < f) + Lemma by_invariant_fuel inv P measure f s0 + (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> if test s then inv (body s) /\ measure (body s) < measure s else P s) : P (while f s0). Proof. rewrite eq_loop. - eapply silent.by_invariant; eauto; []; intros s H; cbv [lbody]. + eapply silent.by_invariant_fuel; eauto; []; intros s H; cbv [lbody]. specialize (step s H); destruct (test s); eauto. Qed. + + Lemma by_invariant (inv P:_->Prop) measure s0 + (init : inv s0) + (step : forall s, inv s -> if test s + then inv (body s) /\ measure (body s) < measure s + else P s) + : P (while (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. Context (body_cps : state ~> state). Fixpoint while_cps f s :~> state := - match f with - | O => return s - | S f => - if test s - then s <- body_cps s; while_cps f s - else return s - end. + if test s + then + s <- body_cps s; + match f with + | O => return s + | S f =>while_cps f s + end + else return s. Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). Lemma loop_cps_ok n s {R} f : while_cps n s R f = f (while n s). Proof. - revert s; induction n; intros s; [reflexivity|]. - cbn; break_match; - cbv [cpscall cpsreturn]; rewrite ?body_cps_ok, ?IHn; reflexivity. + revert s; induction n; intros s; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps_ok + | _ => progress rewrite ?IHn + | _ => progress inversion_sum + | _ => progress break_match + | _ => reflexivity + end. Qed. End While. End while. -- cgit v1.2.3 From 39ca7c56d4d2f50f19ab50d55bf6f836ae4cfe4f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Mar 2018 19:36:26 -0400 Subject: cleanup2 --- src/Curves/Montgomery/XZProofs.v | 55 ++++++++++----------- src/Experiments/Loops.v | 102 +++++++++++++++++++++++++++++++-------- 2 files changed, 110 insertions(+), 47 deletions(-) (limited to 'src/Experiments/Loops.v') diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index c17d14b0a..f44e5fc33 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -281,34 +281,34 @@ Module M. Proof. cbv beta delta [M.montladder]. (* [while.by_invariant] expects a goal like [?P (while _ _ _ _)], make it so: *) - lazymatch goal with |- context [while ?t ?b ?l ?i] => pattern (while t b l i) end. - eapply (while.by_invariant + lazymatch goal with |- context [while ?t ?b ?l ?ii] => pattern (while t b l ii) end. + eapply (while.by_invariant_fuel (fun '(x2, z2, x3, z3, swap, i) => (i < scalarbits)%Z /\ z2 = 0 /\ if dec (Logic.eq i (Z.pred scalarbits)) then x3 = 0 else z3 = 0) - (fun s => Z.to_nat (Z.succ (snd s))) (* decreasing measure *) ). - { (* invariant holds in the beginning *) cbn. - split; [lia|split;[reflexivity|t]]. } + (fun s => Z.to_nat (Z.succ (snd s)))). + { split. + (* invariant holds in the beginning *) + { cbn; split; [lia|split;[reflexivity|t]]. } + { (* fuel <= measure *) cbn. rewrite Z.succ_pred. reflexivity. } } { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hz2 Hx3z3]]. destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *) rewrite Z.geb_ge_iff in Hbranch. - { (* if loop continued, invariant is preserved *) - destruct (dec (Logic.eq i (Z.pred scalarbits))). - { (* first loop iteration *) - cbv -[xzladderstep xorb Z.testbit Z.pred dec Z.lt]; - destruct (xorb swap (Z.testbit n i)); - split; [lia|t|lia|t]. } - { (* subsequent loop iterations *) - cbv -[xzladderstep xorb Z.testbit Z.pred dec Z.lt]. - destruct (xorb swap (Z.testbit n i)); - (split; [lia| split; [t| break_match;[lia|t]]]). } } + { split. (* if loop continued, invariant is preserved *) + { destruct (dec (Logic.eq i (Z.pred scalarbits))). + { (* first loop iteration *) + cbv -[xzladderstep xorb Z.testbit Z.pred dec Z.lt]; + destruct (xorb swap (Z.testbit n i)); + split; [lia|t|lia|t]. } + { (* subsequent loop iterations *) + cbv -[xzladderstep xorb Z.testbit Z.pred dec Z.lt]. + destruct (xorb swap (Z.testbit n i)); + (split; [lia| split; [t| break_match;[lia|t]]]). } } + { (* measure decreases *) + cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. } } { (* if loop exited, invariant implies postcondition *) break_match; break_match_hyps; setoid_subst_rel Feq; fsatz. } } - { (* fuel <= measure *) cbn. rewrite Z.succ_pred. reflexivity. } - { (* measure decreases *) intros [? i]. - destruct (i >=? 0)%Z eqn:Hbranch;rewrite Z.geb_ge_iff in Hbranch; [|exact I]. - cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. } Qed. Lemma montladder_correct_nz @@ -325,7 +325,7 @@ Module M. cbv beta delta [M.montladder]. (* [while.by_invariant] expects a goal like [?P (while _ _ _ _)], make it so: *) lazymatch goal with |- context [while ?t ?b ?l ?i] => pattern (while t b l i) end. - eapply (while.by_invariant + eapply (while.by_invariant_fuel (fun '(x2, z2, x3, z3, swap, i) => (i >= -1)%Z /\ projective (pair x2 z2) /\ @@ -337,12 +337,15 @@ Module M. eq q' (to_xz (scalarmult (Z.succ r) P)) /\ ladder_invariant point (scalarmult r P) (scalarmult (Z.succ r) P)) (fun s => Z.to_nat (Z.succ (snd s))) (* decreasing measure *) ). - { (* invariant holds in the beginning *) cbn. - rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by tauto. - repeat split; [lia|t..]. } + { split; cbn. + { (* invariant holds in the beginning *) + rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by tauto. + repeat split; [lia|t..]. } + { (* sufficient fuel *) rewrite Z.succ_pred. reflexivity. } } { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hx2z2 [Hx3z3 [Hq [Hq' Hladder]]]]]. destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *) rewrite Z.geb_ge_iff in Hbranch. + split. { (* if loop continued, invariant is preserved *) let group _ := ltac:(repeat rewrite ?scalarmult_add_l, ?scalarmult_0_l, ?scalarmult_1_l, ?Hierarchy.left_identity, ?Hierarchy.right_identity, ?Hierarchy.associative, ?(Hierarchy.commutative _ P); reflexivity) in destruct (Z.testbit n i) eqn:Hbit in *; @@ -373,16 +376,14 @@ Module M. => refine (proj1 (Proper_ladder_invariant _ _ (reflexivity _) _ _ _ _ _ _) (ladder_invariant_swap _ _ _ H)); group () | |- ?P => match type of P with Prop => split end end. } + { (* measure decreases *) + cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. } { (* if loop exited, invariant implies postcondition *) destruct_head' @and; autorewrite with cancel_pair in *. replace i with ((-(1))%Z) in * by lia; clear Hi Hbranch. rewrite Z.succ_m1, Z.shiftr_0_r in *. destruct swap eqn:Hswap; rewrite <-!to_x_inv00 by assumption; eauto using projective_to_xz, proper_to_x_projective. } } - { (* fuel <= measure *) cbn. rewrite Z.succ_pred. reflexivity. } - { (* measure decreases *) intros [? i]. - destruct (i >=? 0)%Z eqn:Hbranch;rewrite Z.geb_ge_iff in Hbranch; [|exact I]. - cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. } Qed. (* Using montladder_correct_0 in the combined correctness theorem requires diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v index e5c8bf2ef..56b27dac7 100644 --- a/src/Experiments/Loops.v +++ b/src/Experiments/Loops.v @@ -98,17 +98,17 @@ Module Import core. end. Qed. - Lemma loop_fuel_0 s : loop 0 s = body s. + Local Lemma loop_fuel_0 s : loop 0 s = body s. Proof. cbv; break_match; reflexivity. Qed. - Lemma loop_fuel_S_first n s : loop (S n) s = + Local Lemma loop_fuel_S_first n s : loop (S n) s = match body s with | inl a => loop n a | inr b => inr b end. Proof. reflexivity. Qed. - Lemma loop_fuel_S_last n s : loop (S n) s = + Local Lemma loop_fuel_S_last n s : loop (S n) s = match loop n s with | inl a => body a | inr b => loop n s @@ -119,7 +119,7 @@ Module Import core. { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } Qed. - Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. + Local Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. Proof. revert H; revert b; revert s; induction n; intros ? ? H. { cbn [loop nat_rect] in *; break_match_hyps; congruence_sum; congruence. } @@ -127,7 +127,7 @@ Module Import core. break_match; congruence_sum; reflexivity. } Qed. - Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. + Local Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. Proof. induction m; intros. { rewrite PeanoNat.Nat.add_0_l. assumption. } @@ -148,7 +148,7 @@ Module Import core. { erewrite loop_fuel_S_stable by eassumption. congruence. } } Qed. - Lemma by_invariant_fuel' (inv P:_->Prop) measure f s0 + Local Lemma by_invariant_fuel' (inv:_->Prop) measure P f s0 (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -167,7 +167,7 @@ Module Import core. exact (IHf a ltac:(split; (assumption || lia))). } Qed. - Lemma by_invariant_fuel (inv P:_->Prop) measure f s0 + Lemma by_invariant_fuel (inv:_->Prop) measure P f s0 (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -175,11 +175,11 @@ Module Import core. end) : exists b, loop f s0 = inr b /\ P b. Proof. - pose proof (by_invariant_fuel' inv P measure f s0); + pose proof (by_invariant_fuel' inv measure P f s0); specialize_by assumption; break_match_hyps; [contradiction|eauto]. Qed. - Lemma by_invariant (inv P:_->Prop) measure s0 + Lemma by_invariant (inv:_->Prop) measure P s0 (init : inv s0) (step : forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -257,7 +257,7 @@ Module Import core. rewrite loop_fuel_S_last, H in Hs'; congruence. } Qed. - Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) + Local Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) : exists inv measure, (inv s0 /\ measure s0 <= f) /\ forall s, inv s -> match body s with @@ -294,7 +294,7 @@ Module Import core. rewrite (loop_fuel_irrelevant _ _ _ _ _ HH Hs); congruence. } } Qed. - Lemma invariant_iff f s0 P : + Lemma invariant_iff P f s0 : (exists b, loop f s0 = inr b /\ P b) <-> (exists inv measure, @@ -308,6 +308,13 @@ Module Import core. eauto using invariant_complete, by_invariant_fuel. Qed. End Loops. + + Global Arguments loop_cps_ok {A B body body_cps}. + Global Arguments loop_cps2_ok {A B body body_cps2}. + Global Arguments by_invariant_fuel {A B body} inv measure P. + Global Arguments by_invariant {A B body} inv measure P. + Global Arguments invariant_iff {A B body} P f s0. + Global Arguments iterations_required_correct {A B body} fuel s. End core. Module default. @@ -319,7 +326,7 @@ Module default. | inr s => s end. - Lemma by_invariant_fuel inv (P:_->Prop) measure f s0 + Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 (init : inv s0 /\ measure s0 <= f) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -327,12 +334,12 @@ Module default. end) : P (loop f s0). Proof. - edestruct (by_invariant_fuel body inv P measure f s0) as [x [HA HB]]; eauto; []. + edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [HA HB]]; eauto; []. apply (f_equal (fun r : A + B => match r with inl s => default | inr s => s end)) in HA. cbv [loop]; break_match; congruence. Qed. - Lemma by_invariant (inv P:_->Prop) measure s0 + Lemma by_invariant (inv:_->Prop) measure P s0 (init : inv s0) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -341,6 +348,8 @@ Module default. : P (loop (measure s0) s0). Proof. eapply by_invariant_fuel; eauto. Qed. End Default. + Global Arguments by_invariant_fuel {A B default body} inv measure P. + Global Arguments by_invariant {A B default body} inv measure P. End default. Module silent. @@ -352,7 +361,7 @@ Module silent. | inr s => s end. - Lemma by_invariant_fuel inv (P:_->Prop) measure f s0 + Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 (init : inv s0 /\ measure s0 <= f) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -360,12 +369,12 @@ Module silent. end) : P (loop f s0). Proof. - edestruct (by_invariant_fuel body inv P measure f s0) as [x [A B]]; eauto; []. + edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [A B]]; eauto; []. apply (f_equal (fun r : state + state => match r with inl s => s | inr s => s end)) in A. cbv [loop]; break_match; congruence. Qed. - Lemma by_invariant (inv P:_->Prop) measure s0 + Lemma by_invariant (inv:_->Prop) measure P s0 (init : inv s0) (step: forall s, inv s -> match body s with | inl s' => inv s' /\ measure s' < measure s @@ -374,6 +383,9 @@ Module silent. : P (loop (measure s0) s0). Proof. eapply by_invariant_fuel; eauto. Qed. End Silent. + + Global Arguments by_invariant_fuel {state body} inv measure P. + Global Arguments by_invariant {state body} inv measure P. End silent. Module while. @@ -406,7 +418,7 @@ Module while. end. Qed. - Lemma by_invariant_fuel inv P measure f s0 + Lemma by_invariant_fuel inv measure P f s0 (init : inv s0 /\ measure s0 <= f) (step : forall s, inv s -> if test s then inv (body s) /\ measure (body s) < measure s @@ -418,7 +430,7 @@ Module while. specialize (step s H); destruct (test s); eauto. Qed. - Lemma by_invariant (inv P:_->Prop) measure s0 + Lemma by_invariant (inv:_->Prop) measure P s0 (init : inv s0) (step : forall s, inv s -> if test s then inv (body s) /\ measure (body s) < measure s @@ -454,6 +466,8 @@ Module while. end. Qed. End While. + Global Arguments by_invariant_fuel {state test body} inv measure P. + Global Arguments by_invariant {state test body} inv measure P. End while. Notation while := while.while. @@ -461,4 +475,52 @@ Definition for2 {state} (test : state -> bool) (increment body : state -> state) := while test (fun s => let s := body s in increment s). Definition for3 {state} init test increment body fuel := - @for2 state test increment body fuel init. \ No newline at end of file + @for2 state test increment body fuel init. + +(* TODO: we probably want notations for these. here are some ideas: *) + +(* notation for core.loop_cps2: + loop '(state1, state2, ...) := init + decreasing measure {{ + continue: + body + }} break; + cont +where + continue, break are binders (for continuations passed by core.loop_cps2) + state1, state2 are binders for tuple fields + measure is a function of state1, state2, ... (or the tuple bound by them) + body is a function of continue_label, state1, state2, ... + cont is the contiuation passed to core.loop_cps2 + "loop" and "decreasing" are delimiters +*) + +(* notation for while.while_cps: + + loop '(state1, state2, ...) := init + while test + decreasing measure {{ + continue: + body + }}; + cont +where + state1, state2, continue are binders + body is a function of all of them + test and measure are functions of state1, state2 (or the tuple bound by them) + "loop", "while" and "decreasing" are delimiters + cont is a continuation to the entire loop + *) + + +(* idea for notation for some for-like loop: +loop '(state1, state2) := init +for (i := 0; i Date: Mon, 26 Mar 2018 19:39:38 -0400 Subject: move Loops from Experiments to Util --- _CoqProject | 2 +- src/Curves/Montgomery/XZ.v | 2 +- src/Curves/Montgomery/XZProofs.v | 2 +- src/Experiments/Loops.v | 526 --------------------------------------- src/Util/Loops.v | 526 +++++++++++++++++++++++++++++++++++++++ 5 files changed, 529 insertions(+), 529 deletions(-) delete mode 100644 src/Experiments/Loops.v create mode 100644 src/Util/Loops.v (limited to 'src/Experiments/Loops.v') diff --git a/_CoqProject b/_CoqProject index 8c376eb88..44f15cb76 100644 --- a/_CoqProject +++ b/_CoqProject @@ -240,7 +240,6 @@ src/Curves/Weierstrass/Affine.v src/Curves/Weierstrass/AffineProofs.v src/Curves/Weierstrass/Jacobian.v src/Curves/Weierstrass/Projective.v -src/Experiments/Loops.v src/Experiments/SimplyTypedArithmetic.v src/LegacyArithmetic/ArchitectureToZLike.v src/LegacyArithmetic/ArchitectureToZLikeProofs.v @@ -6465,6 +6464,7 @@ src/Util/LetIn.v src/Util/LetInMonad.v src/Util/ListUtil.v src/Util/Logic.v +src/Util/Loops.v src/Util/NUtil.v src/Util/NatUtil.v src/Util/Notations.v diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v index 336ee6b95..88e1d7398 100644 --- a/src/Curves/Montgomery/XZ.v +++ b/src/Curves/Montgomery/XZ.v @@ -2,7 +2,7 @@ Require Import Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations. Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.Decidable. -Require Import Crypto.Experiments.Loops. +Require Import Crypto.Util.Loops. Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine. Module M. diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index f44e5fc33..650ed6920 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -258,7 +258,7 @@ Module M. Local Notation montladder := (M.montladder(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)(Fzero:=Fzero)(Fone:=Fone)(Finv:=Finv)(cswap:=fun b x y => if b then pair y x else pair x y)). Local Notation scalarmult := (@ScalarMult.scalarmult_ref Mpoint Madd M.zero Mopp). - Import Crypto.Experiments.Loops. + Import Crypto.Util.Loops. Import Coq.ZArith.BinInt. Lemma to_x_inv00 (HFinv:Finv 0 = 0) x z : to_x (pair x z) = x * Finv z. diff --git a/src/Experiments/Loops.v b/src/Experiments/Loops.v deleted file mode 100644 index 56b27dac7..000000000 --- a/src/Experiments/Loops.v +++ /dev/null @@ -1,526 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Lia. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.LetIn. - -Require Import Crypto.Util.CPSNotations. - -Module Import core. - Section Loops. - Context {A B : Type} (body : A -> A + B). - - (* the fuel parameter is only present to allow defining a loop - without proving its termination. The loop body does not have - access to the amount of remaining fuel, and thus increasing fuel - beyond termination cannot change the behavior. fuel counts full - loops -- the one that exacutes "break" is not included *) - - Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := - let s := body s in - match s with - | inl a => - match fuel with - | O => inl a - | S fuel' => loop fuel' a - end - | inr b => inr b - end. - - Context (body_cps : A ~> A + B). - - Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := - s <- body_cps s; - match s with - | inl a => - match fuel with - | O => return (inl a) - | S fuel' => loop_cps fuel' a - end - | inr b => return (inr b) - end. - - Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). - Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). - Proof. - revert f; revert R; revert s; induction n; - repeat match goal with - | _ => progress intros - | _ => progress cbv [cpsreturn cpscall] in * - | _ => progress cbn - | _ => progress rewrite ?body_cps_ok - | _ => progress rewrite ?IHn - | _ => progress break_match - | _ => reflexivity - end. - Qed. - - Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). - Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := - body_cps2 s R - (fun a => - match fuel with - | O => timeout a - | S fuel' => @loop_cps2 fuel' a R timeout ret - end) - (fun b => ret b). - - Context (body_cps2_ok : forall s {R} continue break, - body_cps2 s R continue break = - match body s with - | inl a => continue a - | inr b => break b - end). - Lemma loop_cps2_ok n s {R} (timeout ret : _ -> R) : - @loop_cps2 n s R timeout ret = - match loop n s with - | inl a => timeout a - | inr b => ret b - end. - Proof. - revert timeout; revert ret; revert R; revert s; induction n; - repeat match goal with - | _ => progress intros - | _ => progress cbv [cpsreturn cpscall] in * - | _ => progress cbn - | _ => progress rewrite ?body_cps2_ok - | _ => progress rewrite ?IHn - | _ => progress inversion_sum - | _ => progress subst - | _ => progress break_match - | _ => reflexivity - end. - Qed. - - Local Lemma loop_fuel_0 s : loop 0 s = body s. - Proof. cbv; break_match; reflexivity. Qed. - - Local Lemma loop_fuel_S_first n s : loop (S n) s = - match body s with - | inl a => loop n a - | inr b => inr b - end. - Proof. reflexivity. Qed. - - Local Lemma loop_fuel_S_last n s : loop (S n) s = - match loop n s with - | inl a => body a - | inr b => loop n s - end. - Proof. - revert s; induction n; cbn; intros s. - { break_match; reflexivity. } - { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } - Qed. - - Local Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. - Proof. - revert H; revert b; revert s; induction n; intros ? ? H. - { cbn [loop nat_rect] in *; break_match_hyps; congruence_sum; congruence. } - { rewrite loop_fuel_S_last. - break_match; congruence_sum; reflexivity. } - Qed. - - Local Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. - Proof. - induction m; intros. - { rewrite PeanoNat.Nat.add_0_l. assumption. } - { rewrite PeanoNat.Nat.add_succ_l. - erewrite loop_fuel_S_stable; eauto. } - Qed. - - Lemma loop_fuel_irrelevant n m s bn bm - (Hn : loop n s = inr bn) - (Hm : loop m s = inr bm) - : bn = bm. - Proof. - destruct (Compare_dec.le_le_S_dec n m) as [H|H]; - destruct (PeanoNat.Nat.le_exists_sub _ _ H) as [d [? _]]; subst. - { erewrite loop_fuel_add_stable in Hm by eassumption; congruence. } - { erewrite loop_fuel_add_stable in Hn. - { congruence_sum. reflexivity. } - { erewrite loop_fuel_S_stable by eassumption. congruence. } } - Qed. - - Local Lemma by_invariant_fuel' (inv:_->Prop) measure P f s0 - (init : inv s0 /\ measure s0 <= f) - (step : forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : match loop f s0 with - | inl a => False - | inr s => P s - end. - Proof. - revert dependent s0; induction f; intros; destruct_head'_and. - { specialize (step s0 H); cbv; break_innermost_match; [lia|assumption]. } - { rewrite loop_fuel_S_first. - specialize (step s0 H); destruct (body s0); [|assumption]. - destruct step. - exact (IHf a ltac:(split; (assumption || lia))). } - Qed. - - Lemma by_invariant_fuel (inv:_->Prop) measure P f s0 - (init : inv s0 /\ measure s0 <= f) - (step : forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : exists b, loop f s0 = inr b /\ P b. - Proof. - pose proof (by_invariant_fuel' inv measure P f s0); - specialize_by assumption; break_match_hyps; [contradiction|eauto]. - Qed. - - Lemma by_invariant (inv:_->Prop) measure P s0 - (init : inv s0) - (step : forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : exists b, loop (measure s0) s0 = inr b /\ P b. - Proof. eapply by_invariant_fuel; eauto. Qed. - - (* Completeness proof *) - - Definition iterations_required fuel s : option nat := - nat_rect _ None - (fun n r => - match r with - | Some _ => r - | None => - match loop n s with - | inl a => None - | inr b => Some n - end - end - ) fuel. - - Lemma iterations_required_correct fuel s : - (forall m, iterations_required fuel s = Some m -> - m < fuel /\ - exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) - /\ - (iterations_required fuel s = None -> forall n, n < fuel -> exists a, loop n s = inl a). - Proof. - induction fuel; intros. - { cbn. split; intros; inversion_option; lia. } - { change (iterations_required (S fuel) s) - with (match iterations_required fuel s with - | None => match loop fuel s with - | inl _ => None - | inr _ => Some fuel - end - | Some _ => iterations_required fuel s - end) in *. - destruct (iterations_required fuel s) in *. - { split; intros; inversion_option; subst. - destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } - { destruct (loop fuel s) eqn:HSf; split; intros; inversion_option; subst. - { intros. destruct (PeanoNat.Nat.eq_dec n fuel); subst; eauto; []. - assert (n < fuel) by lia. eapply IHfuel; congruence. } - { split; [lia|]. - exists b; intros; split; intros. - { eapply IHfuel; congruence || lia. } - { eapply PeanoNat.Nat.le_exists_sub in H; destruct H as [?[]]; subst. - eauto using loop_fuel_add_stable. } } } } - Qed. - - Lemma iterations_required_step fuel s s' n - (Hs : iterations_required fuel s = Some (S n)) - (Hstep : body s = inl s') - : iterations_required fuel s' = Some n. - Proof. - eapply iterations_required_correct in Hs. - destruct Hs as [Hn [b Hs]]. - pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. - rewrite loop_fuel_S_first, Hstep in H. - destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. - { eapply iterations_required_correct in Hs'; destruct Hs' as [Hx Hs']. - destruct Hs' as [b' Hs']. - destruct (Compare_dec.le_lt_dec n x) as [Hc|Hc]. - { destruct (Compare_dec.le_lt_dec x n) as [Hc'|Hc']; try lia; []. - destruct (proj1 (Hs' n) Hc'); congruence. } - { destruct (proj1 (Hs (S x)) ltac:(lia)) as [? HX]. - rewrite loop_fuel_S_first, Hstep in HX. - pose proof (proj2 (Hs' x) ltac:(lia)). - congruence. } } - { eapply iterations_required_correct in Hs'; destruct Hs' as [? Hs']; - [|exact Hn]. - rewrite loop_fuel_S_last, H in Hs'; congruence. } - Qed. - - Local Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) - : exists inv measure, - (inv s0 /\ measure s0 <= f) - /\ forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end. - Proof. - set (measure s := match iterations_required (S f) s with None => 0 | Some n => n end). - exists (fun s => match loop (measure s) s with - | inl a => False - | inr r => r = b end). - exists (measure); split; [ |repeat match goal with |- _ /\ _ => split end..]. - { cbv [measure]. - destruct (iterations_required (S f) s0) eqn:Hs0; - eapply iterations_required_correct in Hs0; - [ .. | exact (ltac:(lia):f - (exists inv measure, - (inv s0 /\ measure s0 <= f) - /\ forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end). - Proof. - repeat (intros || split || destruct_head'_ex || destruct_head'_and); - eauto using invariant_complete, by_invariant_fuel. - Qed. - End Loops. - - Global Arguments loop_cps_ok {A B body body_cps}. - Global Arguments loop_cps2_ok {A B body body_cps2}. - Global Arguments by_invariant_fuel {A B body} inv measure P. - Global Arguments by_invariant {A B body} inv measure P. - Global Arguments invariant_iff {A B body} P f s0. - Global Arguments iterations_required_correct {A B body} fuel s. -End core. - -Module default. - Section Default. - Context {A B} (default : B) (body : A -> A + B). - Definition loop fuel s : B := - match loop body fuel s with - | inl s => default - | inr s => s - end. - - Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 - (init : inv s0 /\ measure s0 <= f) - (step: forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : P (loop f s0). - Proof. - edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [HA HB]]; eauto; []. - apply (f_equal (fun r : A + B => match r with inl s => default | inr s => s end)) in HA. - cbv [loop]; break_match; congruence. - Qed. - - Lemma by_invariant (inv:_->Prop) measure P s0 - (init : inv s0) - (step: forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : P (loop (measure s0) s0). - Proof. eapply by_invariant_fuel; eauto. Qed. - End Default. - Global Arguments by_invariant_fuel {A B default body} inv measure P. - Global Arguments by_invariant {A B default body} inv measure P. -End default. - -Module silent. - Section Silent. - Context {state} (body : state -> state + state). - Definition loop fuel s : state := - match loop body fuel s with - | inl s => s - | inr s => s - end. - - Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 - (init : inv s0 /\ measure s0 <= f) - (step: forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : P (loop f s0). - Proof. - edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [A B]]; eauto; []. - apply (f_equal (fun r : state + state => match r with inl s => s | inr s => s end)) in A. - cbv [loop]; break_match; congruence. - Qed. - - Lemma by_invariant (inv:_->Prop) measure P s0 - (init : inv s0) - (step: forall s, inv s -> match body s with - | inl s' => inv s' /\ measure s' < measure s - | inr s' => P s' - end) - : P (loop (measure s0) s0). - Proof. eapply by_invariant_fuel; eauto. Qed. - End Silent. - - Global Arguments by_invariant_fuel {state body} inv measure P. - Global Arguments by_invariant {state body} inv measure P. -End silent. - -Module while. - Section While. - Context {state} - (test : state -> bool) - (body : state -> state). - - Fixpoint while f s := - if test s - then - let s := body s in - match f with - | O => s - | S f => while f s - end - else s. - - Local Definition lbody := fun s => if test s then inl (body s) else inr s. - - Lemma eq_loop f s : while f s = silent.loop lbody f s. - Proof. - revert s; induction f; intros s; - repeat match goal with - | _ => progress cbn in * - | _ => progress cbv [silent.loop lbody] in * - | _ => rewrite IHf - | _ => progress break_match - | _ => congruence - end. - Qed. - - Lemma by_invariant_fuel inv measure P f s0 - (init : inv s0 /\ measure s0 <= f) - (step : forall s, inv s -> if test s - then inv (body s) /\ measure (body s) < measure s - else P s) - : P (while f s0). - Proof. - rewrite eq_loop. - eapply silent.by_invariant_fuel; eauto; []; intros s H; cbv [lbody]. - specialize (step s H); destruct (test s); eauto. - Qed. - - Lemma by_invariant (inv:_->Prop) measure P s0 - (init : inv s0) - (step : forall s, inv s -> if test s - then inv (body s) /\ measure (body s) < measure s - else P s) - : P (while (measure s0) s0). - Proof. eapply by_invariant_fuel; eauto. Qed. - - Context (body_cps : state ~> state). - - Fixpoint while_cps f s :~> state := - if test s - then - s <- body_cps s; - match f with - | O => return s - | S f =>while_cps f s - end - else return s. - - Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). - Lemma loop_cps_ok n s {R} f : while_cps n s R f = f (while n s). - Proof. - revert s; induction n; intros s; - repeat match goal with - | _ => progress intros - | _ => progress cbv [cpsreturn cpscall] in * - | _ => progress cbn - | _ => progress rewrite ?body_cps_ok - | _ => progress rewrite ?IHn - | _ => progress inversion_sum - | _ => progress break_match - | _ => reflexivity - end. - Qed. - End While. - Global Arguments by_invariant_fuel {state test body} inv measure P. - Global Arguments by_invariant {state test body} inv measure P. -End while. -Notation while := while.while. - -Definition for2 {state} (test : state -> bool) (increment body : state -> state) - := while test (fun s => let s := body s in increment s). - -Definition for3 {state} init test increment body fuel := - @for2 state test increment body fuel init. - -(* TODO: we probably want notations for these. here are some ideas: *) - -(* notation for core.loop_cps2: - loop '(state1, state2, ...) := init - decreasing measure {{ - continue: - body - }} break; - cont -where - continue, break are binders (for continuations passed by core.loop_cps2) - state1, state2 are binders for tuple fields - measure is a function of state1, state2, ... (or the tuple bound by them) - body is a function of continue_label, state1, state2, ... - cont is the contiuation passed to core.loop_cps2 - "loop" and "decreasing" are delimiters -*) - -(* notation for while.while_cps: - - loop '(state1, state2, ...) := init - while test - decreasing measure {{ - continue: - body - }}; - cont -where - state1, state2, continue are binders - body is a function of all of them - test and measure are functions of state1, state2 (or the tuple bound by them) - "loop", "while" and "decreasing" are delimiters - cont is a continuation to the entire loop - *) - - -(* idea for notation for some for-like loop: -loop '(state1, state2) := init -for (i := 0; i A + B). + + (* the fuel parameter is only present to allow defining a loop + without proving its termination. The loop body does not have + access to the amount of remaining fuel, and thus increasing fuel + beyond termination cannot change the behavior. fuel counts full + loops -- the one that exacutes "break" is not included *) + + Fixpoint loop (fuel : nat) (s : A) {struct fuel} : A + B := + let s := body s in + match s with + | inl a => + match fuel with + | O => inl a + | S fuel' => loop fuel' a + end + | inr b => inr b + end. + + Context (body_cps : A ~> A + B). + + Fixpoint loop_cps (fuel : nat) (s : A) {struct fuel} :~> A + B := + s <- body_cps s; + match s with + | inl a => + match fuel with + | O => return (inl a) + | S fuel' => loop_cps fuel' a + end + | inr b => return (inr b) + end. + + Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). + Lemma loop_cps_ok n s {R} f : loop_cps n s R f = f (loop n s). + Proof. + revert f; revert R; revert s; induction n; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps_ok + | _ => progress rewrite ?IHn + | _ => progress break_match + | _ => reflexivity + end. + Qed. + + Context (body_cps2 : A -> forall {R}, (A -> R) -> (B -> R) -> R). + Fixpoint loop_cps2 (fuel : nat) (s : A) {R} (timeout:A->R) (ret:B->R) {struct fuel} : R := + body_cps2 s R + (fun a => + match fuel with + | O => timeout a + | S fuel' => @loop_cps2 fuel' a R timeout ret + end) + (fun b => ret b). + + Context (body_cps2_ok : forall s {R} continue break, + body_cps2 s R continue break = + match body s with + | inl a => continue a + | inr b => break b + end). + Lemma loop_cps2_ok n s {R} (timeout ret : _ -> R) : + @loop_cps2 n s R timeout ret = + match loop n s with + | inl a => timeout a + | inr b => ret b + end. + Proof. + revert timeout; revert ret; revert R; revert s; induction n; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps2_ok + | _ => progress rewrite ?IHn + | _ => progress inversion_sum + | _ => progress subst + | _ => progress break_match + | _ => reflexivity + end. + Qed. + + Local Lemma loop_fuel_0 s : loop 0 s = body s. + Proof. cbv; break_match; reflexivity. Qed. + + Local Lemma loop_fuel_S_first n s : loop (S n) s = + match body s with + | inl a => loop n a + | inr b => inr b + end. + Proof. reflexivity. Qed. + + Local Lemma loop_fuel_S_last n s : loop (S n) s = + match loop n s with + | inl a => body a + | inr b => loop n s + end. + Proof. + revert s; induction n; cbn; intros s. + { break_match; reflexivity. } + { destruct (body s); cbn; rewrite <-?IHn; reflexivity. } + Qed. + + Local Lemma loop_fuel_S_stable n s b (H : loop n s = inr b) : loop (S n) s = inr b. + Proof. + revert H; revert b; revert s; induction n; intros ? ? H. + { cbn [loop nat_rect] in *; break_match_hyps; congruence_sum; congruence. } + { rewrite loop_fuel_S_last. + break_match; congruence_sum; reflexivity. } + Qed. + + Local Lemma loop_fuel_add_stable n m s b (H : loop n s = inr b) : loop (m+n) s = inr b. + Proof. + induction m; intros. + { rewrite PeanoNat.Nat.add_0_l. assumption. } + { rewrite PeanoNat.Nat.add_succ_l. + erewrite loop_fuel_S_stable; eauto. } + Qed. + + Lemma loop_fuel_irrelevant n m s bn bm + (Hn : loop n s = inr bn) + (Hm : loop m s = inr bm) + : bn = bm. + Proof. + destruct (Compare_dec.le_le_S_dec n m) as [H|H]; + destruct (PeanoNat.Nat.le_exists_sub _ _ H) as [d [? _]]; subst. + { erewrite loop_fuel_add_stable in Hm by eassumption; congruence. } + { erewrite loop_fuel_add_stable in Hn. + { congruence_sum. reflexivity. } + { erewrite loop_fuel_S_stable by eassumption. congruence. } } + Qed. + + Local Lemma by_invariant_fuel' (inv:_->Prop) measure P f s0 + (init : inv s0 /\ measure s0 <= f) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : match loop f s0 with + | inl a => False + | inr s => P s + end. + Proof. + revert dependent s0; induction f; intros; destruct_head'_and. + { specialize (step s0 H); cbv; break_innermost_match; [lia|assumption]. } + { rewrite loop_fuel_S_first. + specialize (step s0 H); destruct (body s0); [|assumption]. + destruct step. + exact (IHf a ltac:(split; (assumption || lia))). } + Qed. + + Lemma by_invariant_fuel (inv:_->Prop) measure P f s0 + (init : inv s0 /\ measure s0 <= f) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : exists b, loop f s0 = inr b /\ P b. + Proof. + pose proof (by_invariant_fuel' inv measure P f s0); + specialize_by assumption; break_match_hyps; [contradiction|eauto]. + Qed. + + Lemma by_invariant (inv:_->Prop) measure P s0 + (init : inv s0) + (step : forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : exists b, loop (measure s0) s0 = inr b /\ P b. + Proof. eapply by_invariant_fuel; eauto. Qed. + + (* Completeness proof *) + + Definition iterations_required fuel s : option nat := + nat_rect _ None + (fun n r => + match r with + | Some _ => r + | None => + match loop n s with + | inl a => None + | inr b => Some n + end + end + ) fuel. + + Lemma iterations_required_correct fuel s : + (forall m, iterations_required fuel s = Some m -> + m < fuel /\ + exists b, forall n, (n < m -> exists a, loop n s = inl a) /\ (m <= n -> loop n s = inr b)) + /\ + (iterations_required fuel s = None -> forall n, n < fuel -> exists a, loop n s = inl a). + Proof. + induction fuel; intros. + { cbn. split; intros; inversion_option; lia. } + { change (iterations_required (S fuel) s) + with (match iterations_required fuel s with + | None => match loop fuel s with + | inl _ => None + | inr _ => Some fuel + end + | Some _ => iterations_required fuel s + end) in *. + destruct (iterations_required fuel s) in *. + { split; intros; inversion_option; subst. + destruct (proj1 IHfuel _ eq_refl); split; [lia|assumption]. } + { destruct (loop fuel s) eqn:HSf; split; intros; inversion_option; subst. + { intros. destruct (PeanoNat.Nat.eq_dec n fuel); subst; eauto; []. + assert (n < fuel) by lia. eapply IHfuel; congruence. } + { split; [lia|]. + exists b; intros; split; intros. + { eapply IHfuel; congruence || lia. } + { eapply PeanoNat.Nat.le_exists_sub in H; destruct H as [?[]]; subst. + eauto using loop_fuel_add_stable. } } } } + Qed. + + Lemma iterations_required_step fuel s s' n + (Hs : iterations_required fuel s = Some (S n)) + (Hstep : body s = inl s') + : iterations_required fuel s' = Some n. + Proof. + eapply iterations_required_correct in Hs. + destruct Hs as [Hn [b Hs]]. + pose proof (proj2 (Hs (S n)) ltac:(lia)) as H. + rewrite loop_fuel_S_first, Hstep in H. + destruct (iterations_required fuel s') as [x|] eqn:Hs' in *; [f_equal|exfalso]. + { eapply iterations_required_correct in Hs'; destruct Hs' as [Hx Hs']. + destruct Hs' as [b' Hs']. + destruct (Compare_dec.le_lt_dec n x) as [Hc|Hc]. + { destruct (Compare_dec.le_lt_dec x n) as [Hc'|Hc']; try lia; []. + destruct (proj1 (Hs' n) Hc'); congruence. } + { destruct (proj1 (Hs (S x)) ltac:(lia)) as [? HX]. + rewrite loop_fuel_S_first, Hstep in HX. + pose proof (proj2 (Hs' x) ltac:(lia)). + congruence. } } + { eapply iterations_required_correct in Hs'; destruct Hs' as [? Hs']; + [|exact Hn]. + rewrite loop_fuel_S_last, H in Hs'; congruence. } + Qed. + + Local Lemma invariant_complete (P:_->Prop) f s0 b (H:loop f s0 = inr b) (HP:P b) + : exists inv measure, + (inv s0 /\ measure s0 <= f) + /\ forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end. + Proof. + set (measure s := match iterations_required (S f) s with None => 0 | Some n => n end). + exists (fun s => match loop (measure s) s with + | inl a => False + | inr r => r = b end). + exists (measure); split; [ |repeat match goal with |- _ /\ _ => split end..]. + { cbv [measure]. + destruct (iterations_required (S f) s0) eqn:Hs0; + eapply iterations_required_correct in Hs0; + [ .. | exact (ltac:(lia):f + (exists inv measure, + (inv s0 /\ measure s0 <= f) + /\ forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end). + Proof. + repeat (intros || split || destruct_head'_ex || destruct_head'_and); + eauto using invariant_complete, by_invariant_fuel. + Qed. + End Loops. + + Global Arguments loop_cps_ok {A B body body_cps}. + Global Arguments loop_cps2_ok {A B body body_cps2}. + Global Arguments by_invariant_fuel {A B body} inv measure P. + Global Arguments by_invariant {A B body} inv measure P. + Global Arguments invariant_iff {A B body} P f s0. + Global Arguments iterations_required_correct {A B body} fuel s. +End core. + +Module default. + Section Default. + Context {A B} (default : B) (body : A -> A + B). + Definition loop fuel s : B := + match loop body fuel s with + | inl s => default + | inr s => s + end. + + Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 + (init : inv s0 /\ measure s0 <= f) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop f s0). + Proof. + edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [HA HB]]; eauto; []. + apply (f_equal (fun r : A + B => match r with inl s => default | inr s => s end)) in HA. + cbv [loop]; break_match; congruence. + Qed. + + Lemma by_invariant (inv:_->Prop) measure P s0 + (init : inv s0) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. + End Default. + Global Arguments by_invariant_fuel {A B default body} inv measure P. + Global Arguments by_invariant {A B default body} inv measure P. +End default. + +Module silent. + Section Silent. + Context {state} (body : state -> state + state). + Definition loop fuel s : state := + match loop body fuel s with + | inl s => s + | inr s => s + end. + + Lemma by_invariant_fuel inv measure (P:_->Prop) f s0 + (init : inv s0 /\ measure s0 <= f) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop f s0). + Proof. + edestruct (by_invariant_fuel (body:=body) inv measure P f s0) as [x [A B]]; eauto; []. + apply (f_equal (fun r : state + state => match r with inl s => s | inr s => s end)) in A. + cbv [loop]; break_match; congruence. + Qed. + + Lemma by_invariant (inv:_->Prop) measure P s0 + (init : inv s0) + (step: forall s, inv s -> match body s with + | inl s' => inv s' /\ measure s' < measure s + | inr s' => P s' + end) + : P (loop (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. + End Silent. + + Global Arguments by_invariant_fuel {state body} inv measure P. + Global Arguments by_invariant {state body} inv measure P. +End silent. + +Module while. + Section While. + Context {state} + (test : state -> bool) + (body : state -> state). + + Fixpoint while f s := + if test s + then + let s := body s in + match f with + | O => s + | S f => while f s + end + else s. + + Local Definition lbody := fun s => if test s then inl (body s) else inr s. + + Lemma eq_loop f s : while f s = silent.loop lbody f s. + Proof. + revert s; induction f; intros s; + repeat match goal with + | _ => progress cbn in * + | _ => progress cbv [silent.loop lbody] in * + | _ => rewrite IHf + | _ => progress break_match + | _ => congruence + end. + Qed. + + Lemma by_invariant_fuel inv measure P f s0 + (init : inv s0 /\ measure s0 <= f) + (step : forall s, inv s -> if test s + then inv (body s) /\ measure (body s) < measure s + else P s) + : P (while f s0). + Proof. + rewrite eq_loop. + eapply silent.by_invariant_fuel; eauto; []; intros s H; cbv [lbody]. + specialize (step s H); destruct (test s); eauto. + Qed. + + Lemma by_invariant (inv:_->Prop) measure P s0 + (init : inv s0) + (step : forall s, inv s -> if test s + then inv (body s) /\ measure (body s) < measure s + else P s) + : P (while (measure s0) s0). + Proof. eapply by_invariant_fuel; eauto. Qed. + + Context (body_cps : state ~> state). + + Fixpoint while_cps f s :~> state := + if test s + then + s <- body_cps s; + match f with + | O => return s + | S f =>while_cps f s + end + else return s. + + Context (body_cps_ok : forall s {R} f, body_cps s R f = f (body s)). + Lemma loop_cps_ok n s {R} f : while_cps n s R f = f (while n s). + Proof. + revert s; induction n; intros s; + repeat match goal with + | _ => progress intros + | _ => progress cbv [cpsreturn cpscall] in * + | _ => progress cbn + | _ => progress rewrite ?body_cps_ok + | _ => progress rewrite ?IHn + | _ => progress inversion_sum + | _ => progress break_match + | _ => reflexivity + end. + Qed. + End While. + Global Arguments by_invariant_fuel {state test body} inv measure P. + Global Arguments by_invariant {state test body} inv measure P. +End while. +Notation while := while.while. + +Definition for2 {state} (test : state -> bool) (increment body : state -> state) + := while test (fun s => let s := body s in increment s). + +Definition for3 {state} init test increment body fuel := + @for2 state test increment body fuel init. + +(* TODO: we probably want notations for these. here are some ideas: *) + +(* notation for core.loop_cps2: + loop '(state1, state2, ...) := init + decreasing measure {{ + continue: + body + }} break; + cont +where + continue, break are binders (for continuations passed by core.loop_cps2) + state1, state2 are binders for tuple fields + measure is a function of state1, state2, ... (or the tuple bound by them) + body is a function of continue_label, state1, state2, ... + cont is the contiuation passed to core.loop_cps2 + "loop" and "decreasing" are delimiters +*) + +(* notation for while.while_cps: + + loop '(state1, state2, ...) := init + while test + decreasing measure {{ + continue: + body + }}; + cont +where + state1, state2, continue are binders + body is a function of all of them + test and measure are functions of state1, state2 (or the tuple bound by them) + "loop", "while" and "decreasing" are delimiters + cont is a continuation to the entire loop + *) + + +(* idea for notation for some for-like loop: +loop '(state1, state2) := init +for (i := 0; i