-
Notifications
You must be signed in to change notification settings - Fork 3
/
bigenough.v
120 lines (98 loc) · 4.63 KB
/
bigenough.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
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
(****************************************************************************)
(* This is a small library to do epsilon - N reasoning. *)
(* In order to use it, one only has to know the following tactics: *)
(* *)
(* pose_big_enough i == pose a big enough natural number i *)
(* pose_big_modulus m F == pose a function m : F -> nat which should *)
(* provide a big enough return value *)
(* exists_big_modulus m F := pose_big_modulus m F; exists m *)
(* big_enough == replaces a big enough constraint x <= i *)
(* by true and implicity remembers that i should *)
(* be bigger than x. *)
(* close == all "pose" tactics create a dummy subgoal to *)
(* force the user to explictely indicate that all *)
(* constraints have been found *)
(****************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module BigEnough.
Record big_rel_class_of T (leq : rel T) :=
BigRelClass {
leq_big_internal_op : rel T;
bigger_than_op : seq T -> T;
_ : leq_big_internal_op = leq;
_ : forall i s, leq_big_internal_op i (bigger_than_op (i :: s));
_ : forall i j s, leq_big_internal_op i (bigger_than_op s) ->
leq_big_internal_op i (bigger_than_op (j :: s))
}.
Record big_rel_of T := BigRelOf {
leq_big :> rel T;
big_rel_class : big_rel_class_of leq_big
}.
Definition bigger_than_of T (b : big_rel_of T)
(phb : phantom (rel T) b) :=
bigger_than_op (big_rel_class b).
Notation bigger_than leq := (@bigger_than_of _ _ (Phantom (rel _) leq)).
Definition leq_big_internal_of T (b : big_rel_of T)
(phb : phantom (rel T) b) :=
leq_big_internal_op (big_rel_class b).
Notation leq_big_internal leq := (@leq_big_internal_of _ _ (Phantom (rel _) leq)).
Lemma next_bigger_than T (b : big_rel_of T) i j s :
leq_big_internal b i (bigger_than b s) ->
leq_big_internal b i (bigger_than b (j :: s)).
Proof. by case: b i j s => [? []]. Qed.
Lemma instantiate_bigger_than T (b : big_rel_of T) i s :
leq_big_internal b i (bigger_than b (i :: s)).
Proof. by case: b i s => [? []]. Qed.
Lemma leq_big_internalE T (b : big_rel_of T) : leq_big_internal b = leq_big b.
Proof. by case: b => [? []]. Qed.
(* Lemma big_enough T (b : big_rel_of T) i s : *)
(* leq_big_internal b i (bigger_than b s) -> *)
(* leq_big b i (bigger_than b s). *)
(* Proof. by rewrite leq_big_internalE. Qed. *)
Lemma context_big_enough P T (b : big_rel_of T) i s :
leq_big_internal b i (bigger_than b s) ->
P true ->
P (leq_big b i (bigger_than b s)).
Proof. by rewrite leq_big_internalE => ->. Qed.
Definition big_rel_leq_class : big_rel_class_of leq.
Proof.
exists leq (foldr maxn 0%N) => [|i s|i j s /leq_trans->] //;
by rewrite (leq_maxl, leq_maxr).
Qed.
Canonical big_enough_nat := BigRelOf big_rel_leq_class.
Definition closed T (i : T) := {j : T | j = i}.
Ltac close := match goal with
| |- context [closed ?i] =>
instantiate (1 := [::]) in (value of i); exists i
end.
Ltac pose_big_enough i :=
evar (i : nat); suff : closed i; first do
[move=> _; instantiate (1 := bigger_than leq _) in (value of i)].
Ltac pose_big_modulus m F :=
evar (m : F -> nat); suff : closed m; first do
[move=> _; instantiate (1 := (fun e => bigger_than leq _)) in (value of m)].
Ltac exists_big_modulus m F := pose_big_modulus m F; first exists m.
Ltac olddone :=
trivial; hnf; intros; solve
[ do ![solve [trivial | apply: sym_equal; trivial]
| discriminate | contradiction | split]
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].
Ltac big_enough :=
do ?[ apply context_big_enough;
first do [do ?[ now apply instantiate_bigger_than
| apply next_bigger_than]]].
Ltac big_enough_trans :=
match goal with
| [leq_nm : is_true (?n <= ?m)%N |- is_true (?x <= ?m)] =>
apply: leq_trans leq_nm; big_enough; olddone
| _ => big_enough; olddone
end.
Ltac done := do [olddone|big_enough_trans].
End BigEnough.