Commit d2eea5dc authored by Joachim Bard's avatar Joachim Bard

tailrecursive version of forallb

parent 0fcba367
......@@ -60,8 +60,22 @@ Definition checkSubdivsStep e absenv defVars Gamma (PAQ: precond * analysisResul
&& resultLeq e A absenv
end.
Definition forallbTailrec {X: Type} f (l: list X) :=
fold_left (fun acc v => acc && f v) l true.
Lemma forallbTailrec_false_fixpoint X f (l: list X) :
fold_left (fun acc v => acc && f v) l false = false.
Proof. induction l; auto. Qed.
Lemma forallbTailrec_forallb X f (l: list X) :
forallbTailrec f l = forallb f l.
Proof.
induction l; auto; cbn.
destruct (f a); auto using forallbTailrec_false_fixpoint.
Qed.
Definition checkSubdivs e absenv subdivs defVars Gamma :=
forallb (checkSubdivsStep e absenv defVars Gamma) subdivs.
forallbTailrec (checkSubdivsStep e absenv defVars Gamma) subdivs.
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A Q :
checkSubdivs e absenv subdivs defVars Gamma = true ->
......@@ -70,14 +84,10 @@ Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A Q :
resultLeq e A absenv = true.
Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in H.
apply andb_true_iff in H as [H _].
apply andb_true_iff in H as [H1 H2].
now split.
- apply IHsubdivs; auto. cbn in H.
now apply andb_true_iff in H as [_ H ].
unfold checkSubdivs in H.
rewrite forallbTailrec_forallb in H.
eapply forallb_forall in H; eauto.
now apply andb_true_iff in H as [H1 H2].
Qed.
Fixpoint coverIntv iv intvs :=
......@@ -372,7 +382,7 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
let S_qs := map snd subdivs in
covers Piv (sort Ps) && forallb (fun q => SMTLogic_eqb q (snd P)) S_qs.
covers Piv (sort Ps) && forallbTailrec (fun q => SMTLogic_eqb q (snd P)) S_qs.
Lemma checkPreconds_sound (subdivs: list precond) E P :
checkPreconds subdivs P = true ->
......@@ -389,6 +399,7 @@ Proof.
exists P1. split; auto.
rewrite <- Heq1 in H.
split; auto.
rewrite forallbTailrec_forallb in Hqs.
eapply forallb_forall in Hqs.
- eapply SMTLogic_eqb_sound; eauto.
- apply in_map_iff; eauto.
......@@ -398,8 +409,9 @@ Lemma checkPreconds_preVars subdivs P :
checkPreconds subdivs P = true ->
forall P1, In P1 subdivs -> NatSet.Equal (preVars P1) (preVars P).
Proof.
intros chk P1 Hin. Flover_compute.
intros chk P1 Hin. apply andb_true_iff in chk as [L R].
unfold preVars.
rewrite forallbTailrec_forallb in R.
eapply forallb_forall in R.
2: apply in_map_iff; eauto.
erewrite SMTLogic_eqb_varsLogic; eauto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment