Matching Integer Comparisons |
Require Import Arith.
Require Import Omega.
Lemma Match2:
forall (A B: Prop),
{ A } + { B } ->
forall (S: Set) (xA xB: S),
{ x: S | (A /\ x = xA) \/ (B /\ x = xB) }
.
Lemma Match2_diff:
forall (A B: Prop),
{ A } + { B } ->
(A -> ~B) ->
(B -> ~A) ->
forall (S: Set) (xA xB: S),
{ x: S |
(A -> (x = xA)) /\
(B -> (x = xB))
}
.
Lemma Match3:
forall (A B C: Prop),
{ A } + { B } + { C } ->
forall (S: Set) (xA xB xC: S),
{ x: S | (A /\ x = xA) \/ (B /\ x = xB) \/ (C /\ x = xC) }
.
Lemma Match3_diff:
forall (A B C: Prop),
{ A } + { B } + { C } ->
(A -> ~B /\ ~C) ->
(B -> ~A /\ ~C) ->
(C -> ~A /\ ~B) ->
forall (S: Set) (xA xB xC: S),
{ x: S |
(A -> (x = xA)) /\
(B -> (x = xB)) /\
(C -> (x = xC))
}
.
Lemma match_comp_nat3_aux_1:
forall (n m: nat),
(n < m) -> ~(n = m) /\ ~(n > m).
Lemma match_comp_nat3_aux_2:
forall (n m: nat),
(n = m) -> ~(n < m) /\ ~(n > m).
Lemma match_comp_nat3_aux_3:
forall (n m: nat),
(n > m) -> ~(n < m) /\ ~(n = m).
Definition match_comp_nat3 (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A): A :=
match (Match3_diff
(n < m) (n = m) (n > m) (lt_eq_lt_dec n m)
(match_comp_nat3_aux_1 n m)
(match_comp_nat3_aux_2 n m)
(match_comp_nat3_aux_3 n m)
A lt_branch eq_branch gt_branch) with
| (exist x _) => x
end
.
Lemma match_comp_nat3_lt:
forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
(n < m) ->
(match_comp_nat3 n m A lt_branch eq_branch gt_branch) = lt_branch
.
Lemma match_comp_nat3_eq:
forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
(n = m) ->
(match_comp_nat3 n m A lt_branch eq_branch gt_branch) = eq_branch
.
Lemma match_comp_nat3_gt:
forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
(n > m) ->
(match_comp_nat3 n m A lt_branch eq_branch gt_branch) = gt_branch
.
Lemma match_comp_nat2_aux_0:
forall (n m: nat),
{ n < m } + { n >= m }
.
Lemma match_comp_nat2_aux_1:
forall (n m: nat),
(n < m) -> ~(n >= m)
.
Lemma match_comp_nat2_aux_2:
forall (n m: nat),
(n >= m) -> ~(n < m)
.
Definition match_comp_nat2 (n m: nat) (A: Set) (lt_branch ge_branch: A): A :=
match (Match2_diff
(n < m) (n >= m)
(match_comp_nat2_aux_0 n m)
(match_comp_nat2_aux_1 n m)
(match_comp_nat2_aux_2 n m)
A lt_branch ge_branch) with
| (exist x _) => x
end
.
Lemma match_comp_nat2_lt:
forall (n m: nat) (A: Set) (lt_branch ge_branch: A),
(n < m) ->
(match_comp_nat2 n m A lt_branch ge_branch) = lt_branch
.
Lemma match_comp_nat2_ge:
forall (n m: nat) (A: Set) (lt_branch ge_branch: A),
(n >= m) ->
(match_comp_nat2 n m A lt_branch ge_branch) = ge_branch
.