Commit b3fc8947 authored by Heiko Becker's avatar Heiko Becker

Refactor eq_dec in Expressions.v

parent de675bb7
......@@ -777,29 +777,11 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
- apply expCompare_eq_trans.
Defined.
Ltac solve_tac :=
try (left; auto; fail"" );
try (right; hnf; intros; congruence).
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
Proof.
unfold eq.
induction x; destruct y; cbn;
solve_tac.
- destruct (n ?= n0)%nat eqn:?; firstorder.
- destruct m, m0; cbn; solve_tac;
destruct (V_ordered.eq_dec v v0) as [eq_case | eq_case];
rewrite <- V_orderedFacts.compare_eq_iff in eq_case; firstorder.
- destruct u, u0; cbn; solve_tac; apply IHx.
- destruct b, b0; cbn; solve_tac; destruct (IHx1 y1) as [eq_case | eq_case];
try rewrite eq_case; try apply IHx2;
destruct (expCompare x1 y1) eqn:? ; firstorder.
- destruct (IHx1 y1) as [eq_case | eq_case];
try rewrite eq_case; destruct (IHx2 y2) as [eq_case2 | eq_case2];
try rewrite eq_case2; try apply IHx3;
destruct (expCompare x1 y1) eqn:?; try auto;
destruct (expCompare x2 y2) eqn:?; auto.
- destruct m, m0; cbn; solve_tac; apply IHx.
intros. unfold eq. destruct (expCompare x y) eqn:?; try auto.
- right; hnf; intros; congruence.
- right; hnf; intros; congruence.
Defined.
Definition eq_refl : forall x, eq x x.
......
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