-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathArithAux.v
132 lines (121 loc) · 7.38 KB
/
ArithAux.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
Require Import ssreflect ssrbool.
Require Import mathcomp.ssreflect.eqtype.
Require Import mathcomp.ssreflect.ssrnat.
Require Export Ssromega.
CoInductive interval_point x sx y: bool -> bool -> Prop :=
| IP_Left of y <= x : interval_point x sx y true false
| IP_Right of x + sx.+1 <= y : interval_point x sx y false true
| IP_Inside of x < y & y < x + sx.+1 : interval_point x sx y false false.
CoInductive interval_point_inclusive x sx y: bool -> bool -> Prop :=
| IPI_Left of y < x : interval_point_inclusive x sx y true false
| IPI_Right of x + sx <= y : interval_point_inclusive x sx y false true
| IPI_Inside of x <= y & y < x + sx : interval_point_inclusive x sx y false false.
Record ii_choice {Z : Type} := mkIIChoice
{ ii_f12 : Z; (* contained n1 <= n1 + len1 <= n2 <= n2 + len2 *)
ii_f21 : Z; (* contained n2 <= n2 + len2 <= n1 <= n1 + len1 *)
ii_feq : Z; (* coincide *)
ii_f121 : Z; (* contained n1 = n2 <= n2 + len2 <= n1 + len1 *)
ii_f212 : Z; (* contained n2 <= n1 <= n1 + len1 <= n2 + len2 *)
ii_f2121 : Z; (* overlap n2 < n1 <= n2+l2 < n1+l1 *)
ii_f1212 : Z}. (* overlap n1 < n2 <= n1 + len1 < n2 + len2*)
Definition interval_interval_case {Z : Type} (n1 len1 n2 len2 : nat) (c : @ii_choice Z) :=
if ((n1 == n2) && (len1 == len2)) then ii_feq c (* coincide *) else
if (n1 + len1 <= n2) then ii_f12 c (* contained n1 <= n1 + len1 <= n2 <= n2 + len2 *) else
if (n2 + len2 <= n1) then ii_f21 c (* contained n2 <= n2 + len2 <= n1 <= n1 + len1 *) else
if (n1 >= n2) then
if (n1 + len1 <= n2 + len2) then ii_f212 c (* contained n2 <= n1 <= n1 + len1 <= n2 + len2 *) else
if (n1 == n2) then ii_f121 c (* contained n1 = n2 <= n2 + len2 <= n1 + len1 *)
else ii_f2121 c (* overlap n2 < n1 <= n2+l2 < n1+l1 *)
else if (n1 + len1 >= n2 + len2) then ii_f121 c (* contained n1 < n2 <= n2 + len2 <= n1 + len1 *)
else ii_f1212 c (* overlap n1 < n2 <= n1 + len1 < n2 + len2*).
CoInductive interval_cases_analysis {Z : Type} (x sx y sy : nat) (c1 : ii_choice) : Z -> Prop :=
| I_12 of x + sx <= y :
interval_cases_analysis x sx y sy c1 (@ii_f12 Z c1)
| I_21 of y + sy <= x :
interval_cases_analysis x sx y sy c1 (@ii_f21 Z c1)
| I_eq of x == y & sx == sy :
interval_cases_analysis x sx y sy c1 (@ii_feq Z c1)
| I_121 of x <= y & y + sy <= x + sx & ((x != y) \/ sx != sy):
interval_cases_analysis x sx y sy c1 (@ii_f121 Z c1)
| I_212 of y <= x & x + sx <= y + sy & ((x != y) \/ sx != sy):
interval_cases_analysis x sx y sy c1 (@ii_f212 Z c1)
| I_1212 of x < y & y < x + sx & x + sx < y + sy :
interval_cases_analysis x sx y sy c1 (@ii_f1212 Z c1)
| I_2121 of y < x & x < y + sy & y + sy < x + sx :
interval_cases_analysis x sx y sy c1(@ii_f2121 Z c1).
CoInductive interval_interval_case_anal {Z : Type} (x sx y sy : nat) (c1 c2 : ii_choice)
: Z -> Z -> Prop :=
| II_12 of x + sx <= y : interval_interval_case_anal x sx y sy c1 c2 (@ii_f12 Z c1) (@ii_f21 Z c2)
| II_21 of y + sy <= x : interval_interval_case_anal x sx y sy c1 c2 (@ii_f21 Z c1) (@ii_f12 Z c2)
| II_eq of x == y & sx == sy : interval_interval_case_anal x sx y sy c1 c2 (@ii_feq Z c1) (@ii_feq Z c2)
| II_121 of x <= y & y + sy <= x + sx & ((x != y) \/ sx != sy)
: interval_interval_case_anal x sx y sy c1 c2 (@ii_f121 Z c1) (@ii_f212 Z c2)
| II_212 of y <= x & x + sx <= y + sy & ((x != y) \/ sx != sy)
: interval_interval_case_anal x sx y sy c1 c2 (@ii_f212 Z c1) (@ii_f121 Z c2)
| II_1212 of x < y & y < x + sx & x + sx < y + sy :
interval_interval_case_anal x sx y sy c1 c2 (@ii_f1212 Z c1) (@ii_f2121 Z c2)
| II_2121 of y < x & x < y + sy & y + sy < x + sx :
interval_interval_case_anal x sx y sy c1 c2(@ii_f2121 Z c1) (@ii_f1212 Z c2).
Lemma int_ptP x sx y : interval_point x sx y (y <= x) (x + sx.+1 <= y).
Proof. case: (leqP y x) => H; nat_norm.
- move/leq_trans:(H) => /(_ _ (leq_addr sx _)). rewrite leqNgt => /negbTE ->. by constructor.
- case: ltnP => H'; nat_norm; by constructor; nat_norm.
Qed.
Lemma int_pt_incP x sx y : interval_point_inclusive x sx y (y < x) (x + sx <= y).
Proof. case: (leqP x y) => H.
- case: (leqP (x + sx) y) => H'. by apply : IPI_Right. by apply: IPI_Inside.
- move: (H) => /(leq_trans) => /(_ _ (leq_addr sx _)). rewrite ltnNge => /negbTE ->. by apply: IPI_Left.
Qed.
Lemma interval_cases_analysisP {Z : Type} (x sx y sy : nat) (c1 : @ii_choice Z)
: interval_cases_analysis x sx y sy c1 (interval_interval_case x sx y sy c1).
rewrite /interval_interval_case.
case H0: (_ == _) => /=.
case H1: (_ == _) => /=; (try by constructor).
case H2: (_ <= _); (try by constructor).
case H3: (_ <= _); (try by constructor).
case H4: (_ <= _); case H5: (_ <= _); constructor => //; try (right; rewrite H1 //); try ssromega.
case H2: (_ <= _); (try by constructor);
case H3: (_ <= _); (try by constructor);
case H4: (_ <= _); case H5: (_ <= _); constructor => //; try (left; rewrite H0 //); try ssromega.
Qed.
Lemma interval_interval_case_analP {Z : Type} (x sx y sy : nat) (c1 c2 : @ii_choice Z)
: interval_interval_case_anal x sx y sy c1 c2
(interval_interval_case x sx y sy c1) (interval_interval_case y sy x sx c2).
Proof. rewrite /interval_interval_case. rewrite [y == x]eq_sym [sy == sx]eq_sym.
case: (int_pt_incP x sx y).
+ case: (int_pt_incP y sy x).
* move/(leq_ltn_trans) => H /H /ltnW; by rewrite ltnn.
* rewrite eq_sym. move => H H'. move/ltn_eqF: (H') -> => /=. by constructor.
* move=> H1 H2 H3. move/gtn_eqF: (H3) -> => /=; rewrite H1 [x <= y]leqNgt H3 /=.
case: leqP; by constructor => //; left; move/gtn_eqF: H3 => ->.
+ case: ifP.
* move/andP => []; by constructor.
* move: sx => [|sx]. move: sy => [|sy].
- rewrite eq_refl andbT ?addn0 => F. rewrite leq_eqVlt => /orP []; first by rewrite F.
rewrite [y <= x]leqNgt. move=> H; rewrite H. by constructor; rewrite addn0; apply: ltnW.
- move=> _; rewrite addn0 addnS leqNgt => /negbTE. case: ifP;
first by move=> /(leq_ltn_trans _) => /(_ _ (leq_addr sy _)) ->. move=> _ /negbT; rewrite -leqNgt.
by constructor; rewrite addn0.
- move => ?. case: ifP; first by rewrite addnS;
move=> /(leq_trans _) => /(_ _ (leq_addr sy _)) H /(leq_ltn_trans _) => /(_ _ (leq_addr sx _)); rewrite ltnNge H.
by constructor.
+ case: ifP; first by move/andP => []; constructor.
case: sy => [|sy].
* rewrite addn0 [y <= x]leqNgt. case: (ltngtP x y)=> /=.
- move=> H _ _ /ltnW => H'; rewrite H'.
constructor; [apply: ltnW| rewrite ?addn0|left; move/ltn_eqF: H => ->] => //.
- move/ltnW => ? _ ? /ltnW ?. by constructor; rewrite addn0.
- move=> ->; by constructor; rewrite ?addn0.
* case: ifP.
- rewrite addnS => /(leq_ltn_trans _) => /(_ _ (leq_addr sy _)); by rewrite ltnNge => /negbTE ->.
- move/negbT; rewrite -ltnNge. move => H1 H2 H3. rewrite H3. case: ifP.
+ move=> H3'; move/andP: (conj H3 H3'). rewrite -eqn_leq => /eqP Heq. rewrite -Heq in H1. rewrite -Heq in H2.
rewrite -Heq eq_refl. rewrite [x + sx <= _]leqNgt [x + sy.+1 <= _]leqNgt.
case: (ltngtP (x + sx) (x + sy.+1)) => /=.
- constructor => //; by [apply ltnW | right; move:H2; rewrite eq_refl //= => ->].
- constructor => //; by [apply ltnW | right; move:H2; rewrite eq_refl //= => ->].
- by move/eqP; rewrite eqn_add2l; move: H2; rewrite eq_refl => //= ->.
+ move/negbT. rewrite -ltnNge => H. move/ltn_eqF: (H) ->. case: ifP.
- by constructor => //; left; move/ltn_eqF: H => ->.
- move/negbT; rewrite -ltnNge; constructor => //.
Qed.