Commit c9bcf727 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'affine_arithmetic' into 'affine_arithmetic'

Finish validAffineBoundsCmd proof

See merge request AVA/FloVer!8
parents 9c38c892 5c7c85e0
This diff is collapsed.
......@@ -19,11 +19,31 @@ Proof.
functional induction (Q_orderedExps.exprCompare e1 e2); simpl in Heq;
try congruence; try (simpl; f_equal; auto); try (now rewrite <- mTypeEq_compat_eq);
try now apply Nat.compare_eq.
all: admit.
(* - rewrite Q_orderedExps.V_orderedFacts.compare_eq_iff in Heq. *)
(* now apply Qeq_eqR in Heq. *)
(* - now rewrite <- unopEq_compat_eq. *)
Admitted.
- rewrite <- Qeq_alt in Heq.
now apply Qeq_eqR.
- simpl in e3.
apply andb_false_iff in e3.
apply Ndec.Pcompare_Peqb in e6.
apply Ndec.Pcompare_Peqb in Heq.
destruct e3; congruence.
- simpl in e3.
apply andb_false_iff in e3.
apply Ndec.Pcompare_Peqb in e6.
apply Ndec.Pcompare_Peqb in Heq.
destruct e3; congruence.
- unfold unopEq in e5.
destruct u1, u2; congruence.
- simpl in e5.
apply andb_false_iff in e5.
apply Ndec.Pcompare_Peqb in e8.
apply Ndec.Pcompare_Peqb in Heq.
destruct e5; congruence.
- simpl in e5.
apply andb_false_iff in e5.
apply Ndec.Pcompare_Peqb in e8.
apply Ndec.Pcompare_Peqb in Heq.
destruct e5; congruence.
Qed.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
......
......@@ -645,7 +645,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
rewrite G; auto. }
Defined.
Lemma eq_compat: Proper (eq ==> eq ==> iff) eq.
Instance eq_compat: Proper (eq ==> eq ==> iff) eq.
Proof.
unfold Proper; hnf.
intros e1; induction e1;
......
......@@ -40,7 +40,7 @@ Proof.
pose proof (validAffineBounds_sound) as sound_affine.
assert ((forall e : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e iexpmap = Some af) ->
checked_expressions A E Gamma e iexpmap inoise imap)) as Hchecked
checked_expressions A E Gamma (usedVars f) NatSet.empty e iexpmap inoise imap)) as Hchecked
by (intros e Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
rewrite FloverMapFacts.P.F.empty_o in Hein;
congruence).
......
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