From bf5f1fb2b5dcf60bdeedc80273248e6a8797fcd4 Mon Sep 17 00:00:00 2001 From: Joachim Bard Date: Wed, 13 Feb 2019 16:22:59 +0100 Subject: [PATCH] fixing final proof for expressions --- coq/Expressions.v | 66 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 62 insertions(+), 4 deletions(-) diff --git a/coq/Expressions.v b/coq/Expressions.v index ca878de..d7c30d8 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1074,9 +1074,67 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType. - apply nat_compare_lt in c1. apply nat_compare_lt in c2. assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega). now rewrite c3. } - { admit. } - { admit. } - { admit. } + { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence. + - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst. + rewrite Nat.compare_refl. + apply mTypeEq_compat_eq in Heqb. subst. + rewrite Heqb0. auto. + - apply Nat.compare_eq in c1. subst. + rewrite c2. now destruct (mTypeEq m m1). + - apply Nat.compare_eq in c2. subst. + rewrite c1. now destruct (mTypeEq m m1). + - apply nat_compare_lt in c1. apply nat_compare_lt in c2. + assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega). + rewrite c3. now destruct (mTypeEq m m1). } + { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence. + - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst. + rewrite Nat.compare_refl. + apply mTypeEq_compat_eq in Heqb0. subst. + rewrite Heqb. auto. + - apply Nat.compare_eq in c1. subst. + rewrite c2. now destruct (mTypeEq m m1). + - apply Nat.compare_eq in c2. subst. + rewrite c1. now destruct (mTypeEq m m1). + - apply nat_compare_lt in c1. apply nat_compare_lt in c2. + assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega). + rewrite c3. now destruct (mTypeEq m m1). } + { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence. + - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst. + rewrite Nat.compare_refl. + destruct (mTypeEq m m1) eqn:?. + + type_conv. + destruct (morePrecise m1 m0) eqn:prec1; + destruct (morePrecise m0 m1) eqn:prec2; + destruct m0, m1; simpl in *; try congruence; try auto; + destruct (w ?= w0) eqn:case_w0; rewrite Pos.compare_antisym in lt_e1_e2; + rewrite case_w0 in *; cbn in *; try congruence; + rewrite N.compare_antisym, lt_e2_e3 in lt_e1_e2; cbn in *; congruence. + + type_conv; subst. + destruct (morePrecise m1 m0) eqn:prec1; + destruct (morePrecise m0 m1) eqn:prec2; + destruct m, m0, m1; simpl in *; try congruence; try auto; + destruct (w ?= w0) eqn:case_w0; destruct (w0 ?= w1) eqn:case_w1; + try (apply Ndec.Pcompare_Peqb in case_w0); + try (apply Ndec.Pcompare_Peqb in case_w1); + try rewrite Pos.eqb_eq in *; + try rewrite N.eqb_eq in *; + subst; + try congruence; + try rewrite case_w0; + try rewrite case_w1; try auto; + try rewrite Pos.compare_refl; + try (rewrite N.compare_lt_iff in *; eapply N.lt_trans; eauto); + assert (w ?= w1 = Lt) as G + by (rewrite Pos.compare_lt_iff in *; + eapply Pos.lt_trans; eauto); + rewrite G; auto. + - apply Nat.compare_eq in c1. subst. + rewrite c2. now destruct (mTypeEq m m1). + - apply Nat.compare_eq in c2. subst. + rewrite c1. now destruct (mTypeEq m m1). + - apply nat_compare_lt in c1. apply nat_compare_lt in c2. + assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega). + rewrite c3. now destruct (mTypeEq m m1). } (* destruct (morePrecise m m0); destruct m, m0; try congruence; @@ -1134,7 +1192,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType. try (erewrite exprCompare_eq_lt_is_lt; eauto; fail); try (erewrite exprCompare_lt_eq_is_lt; eauto; fail); try (erewrite IHe1_2; eauto). - Admitted. + Qed. Instance eq_compat: Proper (eq ==> eq ==> iff) eq. Proof. -- GitLab