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
|
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require map.Map.
Axiom matrix : forall (a:Type), Type.
Parameter matrix_WhyType :
forall (a:Type) {a_WT:WhyType a}, WhyType (matrix a).
Existing Instance matrix_WhyType.
Parameter elts:
forall {a:Type} {a_WT:WhyType a}, matrix a ->
Numbers.BinNums.Z -> Numbers.BinNums.Z -> a.
Parameter rows:
forall {a:Type} {a_WT:WhyType a}, matrix a -> Numbers.BinNums.Z.
Parameter columns:
forall {a:Type} {a_WT:WhyType a}, matrix a -> Numbers.BinNums.Z.
Axiom matrix'invariant :
forall {a:Type} {a_WT:WhyType a},
forall (self:matrix a), (0%Z <= (rows self))%Z /\ (0%Z <= (columns self))%Z.
(* Why3 assumption *)
Definition valid_index {a:Type} {a_WT:WhyType a} (a1:matrix a)
(r:Numbers.BinNums.Z) (c:Numbers.BinNums.Z) : Prop :=
((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ (0%Z <= c)%Z /\ (c < (columns a1))%Z.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:matrix a) (r:Numbers.BinNums.Z)
(c:Numbers.BinNums.Z) : a :=
elts a1 r c.
Parameter update:
forall {a:Type} {a_WT:WhyType a}, matrix a -> Numbers.BinNums.Z ->
Numbers.BinNums.Z -> a -> matrix a.
Axiom update'spec'1 :
forall {a:Type} {a_WT:WhyType a},
forall (a1:matrix a) (r:Numbers.BinNums.Z) (c:Numbers.BinNums.Z) (v:a),
((rows (update a1 r c v)) = (rows a1)).
Axiom update'spec'0 :
forall {a:Type} {a_WT:WhyType a},
forall (a1:matrix a) (r:Numbers.BinNums.Z) (c:Numbers.BinNums.Z) (v:a),
((columns (update a1 r c v)) = (columns a1)).
Axiom update'spec :
forall {a:Type} {a_WT:WhyType a},
forall (a1:matrix a) (r:Numbers.BinNums.Z) (c:Numbers.BinNums.Z) (v:a),
((elts (update a1 r c v)) =
(map.Map.set (elts a1) r (map.Map.set (elts a1 r) c v))).
(* Why3 assumption *)
Inductive path: matrix Init.Datatypes.bool -> Numbers.BinNums.Z ->
Numbers.BinNums.Z -> Numbers.BinNums.Z -> Prop :=
| Path_empty :
forall (m:matrix Init.Datatypes.bool) (i:Numbers.BinNums.Z)
(j:Numbers.BinNums.Z) (k:Numbers.BinNums.Z),
((elts m i j) = Init.Datatypes.true) -> path m i j k
| Path_cons :
forall (m:matrix Init.Datatypes.bool) (i:Numbers.BinNums.Z)
(x:Numbers.BinNums.Z) (j:Numbers.BinNums.Z) (k:Numbers.BinNums.Z),
(0%Z <= x)%Z /\ (x < k)%Z -> path m i x k -> path m x j k ->
path m i j k.
Axiom weakening :
forall (m:matrix Init.Datatypes.bool) (i:Numbers.BinNums.Z)
(j:Numbers.BinNums.Z) (k1:Numbers.BinNums.Z) (k2:Numbers.BinNums.Z),
(0%Z <= k1)%Z /\ (k1 <= k2)%Z -> path m i j k1 -> path m i j k2.
Hint Constructors path.
(* Why3 goal *)
Theorem decomposition :
forall (m:matrix Init.Datatypes.bool) (k:Numbers.BinNums.Z),
(0%Z <= k)%Z -> forall (i:Numbers.BinNums.Z) (j:Numbers.BinNums.Z),
path m i j (k + 1%Z)%Z -> path m i j k \/ path m i k k /\ path m k j k.
(* Why3 intros m k h1 i j h2. *)
intros m k hk i j h.
remember (k+1)%Z as t in h.
induction h.
left; apply Path_empty; auto.
subst k0; intuition.
generalize (Z.lt_total x k); intros [c|[c|c]].
left; eauto.
subst; eauto.
auto with zarith.
generalize (Z.lt_total x k); intros [c|[c|c]].
right; eauto.
subst x.
right; eauto.
auto with zarith.
generalize (Z.lt_total x k); intros [c|[c|c]].
right; eauto.
subst; eauto.
auto with zarith.
Qed.
|
