Skip to content

Commit f7db115

Browse files
strubstrub
committed
[stdlib]: remove axioms (int + inductive schemes)
1 parent b8fb10b commit f7db115

File tree

4 files changed

+86
-76
lines changed

4 files changed

+86
-76
lines changed

‎src/ecEnv.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -729,7 +729,7 @@ module MC = struct
729729
let axp = EcPath.prefix (Lazy.force mypath) in
730730
let axp = IPPath (EcPath.pqoname axp name) in
731731
let ax =
732-
{ ax_kind = `Axiom (Ssym.empty, false);
732+
{ ax_kind = `Lemma;
733733
ax_tparams = tv;
734734
ax_spec = cl;
735735
ax_loca = (snd obj).op_loca;
@@ -787,7 +787,7 @@ module MC = struct
787787
let scname = Printf.sprintf "%s_%s" x name in
788788
(scname, { ax_tparams = tyd.tyd_params;
789789
ax_spec = scheme;
790-
ax_kind = `Axiom (Ssym.empty, false);
790+
ax_kind = `Lemma;
791791
ax_loca = loca;
792792
ax_visibility = `NoSmt;
793793
})
@@ -832,7 +832,7 @@ module MC = struct
832832
let scname = Printf.sprintf "%s_ind" x in
833833
(scname, { ax_tparams = tyd.tyd_params;
834834
ax_spec = scheme;
835-
ax_kind = `Axiom (Ssym.empty, false);
835+
ax_kind = `Lemma;
836836
ax_loca = loca;
837837
ax_visibility = `NoSmt;
838838
})
@@ -919,7 +919,7 @@ module MC = struct
919919
let ax = EcSubst.subst_form fsubst ax in
920920
(x, { ax_tparams = [(self, Sp.singleton mypath)];
921921
ax_spec = ax;
922-
ax_kind = `Axiom (Ssym.empty, false);
922+
ax_kind = `Lemma;
923923
ax_loca = loca;
924924
ax_visibility = `NoSmt; }))
925925
tc.tc_axs

‎src/ecScope.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1767,7 +1767,7 @@ module Ty = struct
17671767
let ax = {
17681768
ax_tparams = [];
17691769
ax_spec = f;
1770-
ax_kind = `Axiom (Ssym.empty, false);
1770+
ax_kind = `Lemma;
17711771
ax_visibility = `NoSmt;
17721772
ax_loca = lc;
17731773
} in

‎theories/datatypes/Int.ec‎

Lines changed: 76 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -19,104 +19,104 @@ lemma intind (p:int -> bool):
1919
proof. exact/CoreInt.intind. qed.
2020

2121
(* -------------------------------------------------------------------- *)
22-
axiom addzA : forall x y z, x + (y + z) = (x + y) + z.
23-
axiom addzC : forall x y, x + y = y + x.
24-
axiom addz0 : forall x, x + 0 = x.
25-
axiom add0z : forall x, 0 + x = x.
26-
axiom addzN : forall x, x - x = 0.
27-
axiom addNz : forall x, -x + x = 0.
28-
axiom mulzA : forall x y z, (x * y) * z = x * (y * z).
29-
axiom mulzC : forall x y, x * y = y * x.
30-
axiom mulz1 : forall x, x * 1 = x.
31-
axiom mul1z : forall x, 1 * x = x.
32-
axiom mulzDl : forall x y z, (x + y) * z = x * z + y * z.
33-
axiom mulzDr : forall x y z, x * (y + z) = x * y + x * z.
34-
axiom onez_neq0 : 1 <> 0.
22+
lemma addzA : forall x y z, x + (y + z) = (x + y) + z by smt().
23+
lemma addzC : forall x y, x + y = y + x by smt().
24+
lemma addz0 : forall x, x + 0 = x by smt().
25+
lemma add0z : forall x, 0 + x = x by smt().
26+
lemma addzN : forall x, x - x = 0 by smt().
27+
lemma addNz : forall x, -x + x = 0 by smt().
28+
lemma mulzA : forall x y z, (x * y) * z = x * (y * z) by smt().
29+
lemma mulzC : forall x y, x * y = y * x by smt().
30+
lemma mulz1 : forall x, x * 1 = x by smt().
31+
lemma mul1z : forall x, 1 * x = x by smt().
32+
lemma mulzDl : forall x y z, (x + y) * z = x * z + y * z by smt().
33+
lemma mulzDr : forall x y z, x * (y + z) = x * y + x * z by smt().
34+
lemma onez_neq0 : 1 <> 0 by smt().
3535

3636
(* -------------------------------------------------------------------- *)
37-
axiom lezz : forall x, x <= x.
38-
axiom lez_trans : forall y x z, x <= y => y <= z => x <= z.
39-
axiom ltz_trans : forall y x z, x < y => y < z => x < z.
40-
axiom lez_anti : forall (x y : int), x <= y <= x => x = y.
41-
axiom lez01 : 0 <= 1.
42-
axiom lez_total : forall x y, x <= y \/ y <= x.
37+
lemma lezz : forall x, x <= x by smt().
38+
lemma lez_trans : forall y x z, x <= y => y <= z => x <= z by smt().
39+
lemma ltz_trans : forall y x z, x < y => y < z => x < z by smt().
40+
lemma lez_anti : forall (x y : int), x <= y <= x => x = y by smt().
41+
lemma lez01 : 0 <= 1 by smt().
42+
lemma lez_total : forall x y, x <= y \/ y <= x by smt().
4343

4444
(* -------------------------------------------------------------------- *)
45-
axiom subzz (z : int): z - z = 0.
46-
axiom subz0 (z : int): z - 0 = z.
45+
lemma subzz (z : int): z - z = 0 by smt().
46+
lemma subz0 (z : int): z - 0 = z by smt().
4747

48-
axiom oppzK: forall (x : int), -(-x) = x.
49-
axiom oppz0: -0 = 0.
48+
lemma oppzK: forall (x : int), -(-x) = x by smt().
49+
lemma oppz0: -0 = 0 by smt().
5050

51-
axiom addzCA (x y z : int): x + (y + z) = y + (x + z).
52-
axiom addzAC (x y z : int): (x + y) + z = (x + z) + y.
51+
lemma addzCA (x y z : int): x + (y + z) = y + (x + z) by smt().
52+
lemma addzAC (x y z : int): (x + y) + z = (x + z) + y by smt().
5353

54-
axiom addzI (x y z : int): x + y = x + z => y = z.
55-
axiom addIz (x y z : int): y + x = z + x => y = z.
54+
lemma addzI (x y z : int): x + y = x + z => y = z by smt().
55+
lemma addIz (x y z : int): y + x = z + x => y = z by smt().
5656

57-
axiom addzK (y x : int): (x + y) - y = x.
58-
axiom addKz (y x : int): -y + (y + x) = x.
57+
lemma addzK (y x : int): (x + y) - y = x by smt().
58+
lemma addKz (y x : int): -y + (y + x) = x by smt().
5959

60-
axiom subz_add2r (x y z : int): (x + z) - (y + z) = x - y.
60+
lemma subz_add2r (x y z : int): (x + z) - (y + z) = x - y by smt().
6161

62-
axiom lez_norm_add (x y : int): `|x + y| <= `|x| + `|y|.
62+
lemma lez_norm_add (x y : int): `|x + y| <= `|x| + `|y| by smt().
6363

64-
axiom addz_gt0 (x y : int): 0 < x => 0 < y => 0 < x + y.
64+
lemma addz_gt0 (x y : int): 0 < x => 0 < y => 0 < x + y by smt().
6565

66-
axiom normz_eq0 (x : int): `|x| = 0 => x = 0.
66+
lemma normz_eq0 (x : int): `|x| = 0 => x = 0 by smt().
6767

68-
axiom normzM (x y : int): `|x * y| = `|x| * `|y|.
68+
lemma normzM (x y : int): `|x * y| = `|x| * `|y| by smt().
6969

70-
axiom lez_def (x y : int): x <= y <=> `|y - x| = y - x.
71-
axiom ltz_def (x y : int): x < y <=> ( y <> x /\ x <= y).
70+
lemma lez_def (x y : int): x <= y <=> `|y - x| = y - x by smt().
71+
lemma ltz_def (x y : int): x < y <=> (y <> x /\ x <= y) by smt().
7272

73-
axiom ltzz (z : int): z < z <=> false.
73+
lemma ltzz (z : int): z < z <=> false by smt().
7474

75-
axiom ltzNge (x y : int): (x < y) <=> !(y <= x).
76-
axiom lezNgt (x y : int): (x <= y) <=> !(y < x).
75+
lemma ltzNge (x y : int): (x < y) <=> !(y <= x) by smt().
76+
lemma lezNgt (x y : int): (x <= y) <=> !(y < x) by smt().
7777

78-
axiom neq_ltz (x y : int): (x <> y) <=> (x < y \/ y < x).
79-
axiom eqz_leq (x y : int): (x = y) <=> (x <= y /\ y <= x).
78+
lemma neq_ltz (x y : int): (x <> y) <=> (x < y \/ y < x) by smt().
79+
lemma eqz_leq (x y : int): (x = y) <=> (x <= y /\ y <= x) by smt().
8080

81-
axiom lez_add2l (x y z : int): (x + y <= x + z) <=> (y <= z).
82-
axiom lez_add2r (x y z : int): (y + x <= z + x) <=> (y <= z).
81+
lemma lez_add2l (x y z : int): (x + y <= x + z) <=> (y <= z) by smt().
82+
lemma lez_add2r (x y z : int): (y + x <= z + x) <=> (y <= z) by smt().
8383

84-
axiom ltz_add2l (x y z : int): (x + y < x + z) <=> (y < z).
85-
axiom ltz_add2r (x y z : int): (y + x < z + x) <=> (y < z).
84+
lemma ltz_add2l (x y z : int): (x + y < x + z) <=> (y < z) by smt().
85+
lemma ltz_add2r (x y z : int): (y + x < z + x) <=> (y < z) by smt().
8686

87-
axiom lez_addl (x y : int) : (x <= x + y) = (0 <= y).
88-
axiom lez_addr (x y : int) : (x <= y + x) = (0 <= y).
87+
lemma lez_addl (x y : int) : (x <= x + y) = (0 <= y) by smt().
88+
lemma lez_addr (x y : int) : (x <= y + x) = (0 <= y) by smt().
8989

90-
axiom ltz_addl (x y : int) : (x < x + y) = (0 < y).
91-
axiom ltz_addr (x y : int) : (x < y + x) = (0 < y).
90+
lemma ltz_addl (x y : int) : (x < x + y) = (0 < y) by smt().
91+
lemma ltz_addr (x y : int) : (x < y + x) = (0 < y) by smt().
9292

93-
axiom addz_ge0 (x y : int) : 0 <= x => 0 <= y => 0 <= x + y.
93+
lemma addz_ge0 (x y : int) : 0 <= x => 0 <= y => 0 <= x + y by smt().
9494

95-
axiom lez_add1r (x y : int): (1 + x <= y) = (x < y).
95+
lemma lez_add1r (x y : int): (1 + x <= y) = (x < y) by smt().
9696

97-
axiom subz_ge0 x y : (0 <= y - x) = (x <= y).
98-
axiom subz_gt0 x y : (0 < y - x) = (x < y).
99-
axiom subz_le0 x y : (y - x <= 0) = (y <= x).
100-
axiom subz_lt0 x y : (y - x < 0) = (y < x).
97+
lemma subz_ge0 x y : (0 <= y - x) = (x <= y) by smt().
98+
lemma subz_gt0 x y : (0 < y - x) = (x < y) by smt().
99+
lemma subz_le0 x y : (y - x <= 0) = (y <= x) by smt().
100+
lemma subz_lt0 x y : (y - x < 0) = (y < x) by smt().
101101

102-
axiom oppz_ge0 x : (0 <= - x) = (x <= 0).
103-
axiom oppz_gt0 x : (0 < - x) = (x < 0).
104-
axiom oppz_le0 x : (- x <= 0) = (0 <= x).
105-
axiom oppz_lt0 x : (- x < 0) = (0 < x).
102+
lemma oppz_ge0 x : (0 <= - x) = (x <= 0) by smt().
103+
lemma oppz_gt0 x : (0 < - x) = (x < 0) by smt().
104+
lemma oppz_le0 x : (- x <= 0) = (0 <= x) by smt().
105+
lemma oppz_lt0 x : (- x < 0) = (0 < x) by smt().
106106

107-
axiom lezWP (z1 z2 : int) : (z1 <= z2) || (z2 <= z1).
108-
axiom ltzW (z1 z2 : int) : (z1 < z2) => (z1 <= z2).
107+
lemma lezWP (z1 z2 : int) : (z1 <= z2) || (z2 <= z1) by smt().
108+
lemma ltzW (z1 z2 : int) : (z1 < z2) => (z1 <= z2) by smt().
109109

110-
axiom addz1_neq0 (i : int) : 0 <= i => i+1 <> 0.
111-
axiom add1z_neq0 (i : int) : 0 <= i => 1+i <> 0.
112-
axiom addz1_neqC0 (i : int): 0 <= i => 0 <> i+1.
113-
axiom add1z_neqC0 (i : int): 0 <= i => 0 <> 1+i.
110+
lemma addz1_neq0 (i : int) : 0 <= i => i+1 <> 0 by smt().
111+
lemma add1z_neq0 (i : int) : 0 <= i => 1+i <> 0 by smt().
112+
lemma addz1_neqC0 (i : int): 0 <= i => 0 <> i+1 by smt().
113+
lemma add1z_neqC0 (i : int): 0 <= i => 0 <> 1+i by smt().
114114

115115
hint rewrite addz_neq0 : addz1_neq0 add1z_neq0 addz1_neqC0 add1z_neqC0.
116116

117-
axiom lez_eqVlt : forall x y, (x <= y) <=> ((x = y) \/ (x < y)).
117+
lemma lez_eqVlt : forall x y, (x <= y) <=> ((x = y) \/ (x < y)) by smt().
118118

119-
axiom lez_lt_asym x y : !(x <= y < x).
119+
lemma lez_lt_asym x y : !(x <= y < x) by smt().
120120

121121
(* -------------------------------------------------------------------- *)
122122
lemma natind (p : int -> bool):
@@ -334,10 +334,16 @@ qed.
334334
(* -------------------------------------------------------------------- *)
335335
(* TO BE REMOVED *)
336336
337-
op fold : ('a -> 'a) -> 'a -> int -> 'a.
337+
op [opaque] fold ['a] (f : 'a -> 'a) (x : 'a) (i : int) =
338+
iter i f x.
338339
339-
axiom foldle0 p (f : 'a -> 'a) a: p <= 0 => fold f a p = a.
340-
axiom foldS (f : 'a -> 'a) a n: 0 <= n => fold f a (n+1) = f (fold f a n).
340+
lemma foldle0 (p : int) (f : 'a -> 'a) (a : 'a) :
341+
p <= 0 => fold f a p = a.
342+
proof. by move=> @/fold; apply: iter0. qed.
343+
344+
lemma foldS (f : 'a -> 'a) (a : 'a) (n : int) :
345+
0 <= n => fold f a (n+1) = f (fold f a n).
346+
proof. by move=> @/fold; apply: iterS. qed.
341347
342348
lemma fold0 (f : 'a -> 'a) a: fold f a 0 = a.
343349
proof. by rewrite foldle0. qed.

‎theories/datatypes/List.ec‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3472,7 +3472,11 @@ theory InsertSort.
34723472
proof. by move=> e_ltgt; elim: s => //= x s IHs; apply sorted_insert. qed.
34733473
end InsertSort.
34743474
3475-
op sort (e : 'a -> 'a -> bool) s = InsertSort.sort e s axiomatized by sortE.
3475+
op [opaque] sort (e : 'a -> 'a -> bool) s = InsertSort.sort e s.
3476+
3477+
lemma sortE ['a] (e : 'a -> 'a -> bool) s :
3478+
sort e s = InsertSort.sort e s.
3479+
proof. by rewrite /sort. qed.
34763480

34773481
lemma perm_sort e (s : 'a list): perm_eq (sort e s) s.
34783482
proof. by rewrite sortE /=; apply InsertSort.perm_sort. qed.

0 commit comments

Comments
 (0)