test: grind_guide.lean

tests/lean/grind_guide.lean

@@ -0,0 +1,306 @@
+/-
+`grind` is inspired by automated reasoning techniques developed in the world of Satisfiability Modulo Theories (SMT).
+
+However, it is not an SMT solver and is not designed to solve massive combinatorial problems.
+For example, it would crash if we tried to feed it some of the bit-blasted formulas produced by
+`bv_decide`.
+
+At the core of grind, we use a custom congruence closure algorithm for dependent type theory.
+We accumulate terms that are known to be equal. You should think of it as a blackboard where
+we keep all the facts we know about the current goal.
+Remark: Terms known to be true (false) belong to the equivalence class of the term `True` (`False`).
+-/
+
+set_option grind.warning false -- Disables warning messages stating that `grind` is WIP.
+
+example (a b c : α) (f : α → α) : f a = c → a = b → c = f b := by
+  grind
+
+/-
+`grind` normalizes terms before adding them to the `grind` state.
+Goals:
+- We want to minimize the number of different things we need to handle.
+- We want to canonicalize instances, implicit terms, etc.
+- We want to hash cons terms, i.e., structural equality == pointer equality (performance).
+- ...
+-/
+
+set_option trace.grind.assert true in -- Trace asserted facts
+example : a = 1 + 2 → b = 3 → a = b := by
+  grind
+
+/-
+`grind` applies many "constraint" propagation rules. They are used
+to apply many builtin principles such as
+- Injectivity of constructors.
+- Beta reduction
+- Extensionality theorems.
+- Logical connectives.
+- ...
+-/
+
+set_option trace.grind.eqc true in -- Trace equivalence classes being merged
+example (f : Nat → List Nat) : f a = [1, 2] → f b = [] → a ≠ b := by
+  grind
+
+/-
+`grind` does not case-split like a SMT solver. It uses the structure of the formula,
+and splits on `if-then-else`-expressions, `match`-expressions, inductive predicates
+marked with `[grind cases]`, etc.
+-/
+set_option trace.grind.split true in -- Trace case-splits performed by `grind`
+example : (match x with
+           | 0 => 1
+           | _ + 1 => 2) > 0 := by
+  grind
+
+example : (match x with
+           | 0 => 1
+           | _ + 1 => 2) > 0 := by
+  grind (splits := 0) -- `grind` fails if we don't allow it case-split.
+
+/-
+`grind` shows you the case-splits performed when it fails.
+-/
+example : (match x with
+           | 0 => 1
+           | _ + 1 => 2) > 1 := by
+  grind
+
+/-
+`simp` uses theorems as rewriting rules.
+`grind` instantiates the theorems using E-matching.
+Each theorem is annotated with patterns.
+Whenever, it finds an instance of the pattern modulo
+the equalities in its state, it instantites the theorem.
+There is no rewriting happening. It is just accumulating facts.
+-/
+
+opaque f : Nat → Nat
+opaque g : Nat → Nat
+-- `[grind =]` instructs `grind` to use the left-hand side of the conclusion as the pattern.
+@[grind =] theorem fg : f (g x) = x := sorry
+
+set_option trace.grind.assert true in
+set_option trace.grind.ematch.instance true in
+example : f a = b → a = g c → b = c := by
+  grind
+
+/-
+We have the following variants:
+- `[grind =_]`: use right-hand side of the conclusion.
+- `[grind _=_]`: use both right and left-hand side of the conclusion.
+- `[grind →]`: use terms in the antecedents as patterns. "Forward reasoning"
+- `[grind ←]`: use terms in the conclusion as patterns. "Backward reasoning"
+- `[grind =>]`: look for patterns from left to right.
+- `[grind <=]`: look for patterns from right to left.
+-/
+
+opaque R : Nat → Nat → Prop
+@[grind →] theorem Rtrans : R x y → R y z → R x z := sorry
+@[grind →] theorem Rsymm : R x y → R y x := sorry
+
+set_option trace.grind.assert true in
+example : R a b → R c b → R d c → R a d := by
+  grind
+
+/-
+The attributes above are for convenience.
+If an user wants total control over the selected pattern
+they may use the command `grind_pattern`.
+-/
+
+opaque bla : Nat → Nat
+theorem blaThm : bla (bla x) = bla x := sorry
+
+grind_pattern blaThm => bla (bla x)
+
+set_option trace.grind.assert true in
+example : bla a = b → bla b = b := by
+  grind
+
+
+/-
+We also have
+- `[grind ←=]`: equality driven backward reasoning.
+-/
+
+opaque U : Type
+axiom mul : U → U → U
+axiom one : U
+axiom inv : U → U
+
+/--
+In the following example, `grind` instantiates the theorem
+whenever it learns a disequality `t = s` where `t` or `s` E-matches `inv a`
+-/
+@[grind ←=] theorem inv_of_mul : mul a b = one → inv a = b :=
+  sorry
+
+/-
+Like `simp`, we also have `grind only`
+-/
+example : R a b → R c b → R d c → R a d := by
+  grind only -- `Rtrans` and `Rsymm` were not applied
+
+example : R a b → R c b → R d c → R a d := by
+  grind only [→ Rtrans, → Rsymm]
+
+example : R a b → R c b → R d c → R a d := by
+  grind only [Rtrans, ← Rsymm]
+
+/-
+We also have `grind?`.
+
+We currently do not try to minimize the number of generated arguments, but
+we will do it in the future.
+It behaves like `simp?`. If something was used, it will appear in the result.
+-/
+
+example : R a b → R c b → R d c → R a d := by
+  grind?
+
+
+/-
+We can instruct `grind` to case-split on inductive predicates and types,
+and use the constructors of an inductive predicate as E-matching theorems.
+-/
+
+abbrev Variable := String
+def State := Variable → Nat
+inductive Stmt : Type where
+  | skip : Stmt
+  | assign : Variable → (State → Nat) → Stmt
+  | seq : Stmt → Stmt → Stmt
+  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
+  | whileDo : (State → Prop) → Stmt → Stmt
+infix:60 ";; " => Stmt.seq
+export Stmt (skip assign seq ifThenElse whileDo)
+set_option quotPrecheck false in
+notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
+inductive BigStep : Stmt → State → State → Prop where
+  | skip (s : State) : BigStep skip s s
+  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
+  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
+    BigStep (S;; T) s u
+  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
+    BigStep (ifThenElse B S T) s t
+  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
+    BigStep (ifThenElse B S T) s t
+  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
+    BigStep (whileDo B S) s u
+  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
+notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
+
+example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind [cases BigStep]
+
+theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind [cases BigStep]
+
+theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
+  grind [cases BigStep]
+
+theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
+  grind [cases BigStep, intro BigStep]
+
+example {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
+  grind [BigStep] -- shortcut for `cases BigStep` and `intro BigStep`
+
+/-
+`grind` already has support for offset equalities and inequalities:
+- `x + k ≤ y`, `x ≤ y + k`, `x + k = y`, ... where `k` is a numeral.
+- Efficient algorithm.
+- Very compact proofs.
+- Exhaustive propagation, but it does not case-split on disequalities.
+
+Very effective for examples using the notation `a[i]`
+-/
+
+-- Standard library will be
+attribute [grind =] Array.size_set Array.get_set_eq Array.get_set_ne
+
+example (as bs cs ds : Array α) (v₁ v₂ v₃ : α)
+        (i₁ i₂ i₃ j : Nat)
+        (h₁ : i₁ < as.size)
+        (h₂ : as.set i₁ v₁ = bs)
+        (h₃ : i₂ < bs.size)
+        (h₃ : bs.set i₂ v₂ = cs)
+        (h₄ : i₃ < cs.size)
+        (h₅ : ds = cs.set i₃ v₃)
+        (h₆ : j ≠ i₁ ∧ j ≠ i₂ ∧ i₃ ≠ j)
+        (h₇ : j < ds.size)
+        (h₈ : j < as.size)
+        : ds[j] = as[j] := by
+  set_option diagnostics true in
+  grind
+
+/-
+`grind` has support for splitting on `match`-expressions with overlapping patterns.
+It is quite complex in the dependent case, and many `cast`-operations have to be performed.
+-/
+namespace Ex
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, a :: _ => if a > 1 then 2 else 3
+  | _, _  => 0
+
+example : z = a :: as → y = z → f x y > 0 := by
+  grind [f.eq_def]
+end Ex
+
+/- It gets quite messy with dependent pattern matching. -/
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+
+def h (v w : Vec α n) : Nat :=
+  match v, w with
+  | _, .cons _ (.cons _ _) => 20
+  | .nil, _  => 30
+  | _, _    => 40
+
+example : b = .cons 1 .nil → h a b = 40 := by
+  grind [h.eq_def]
+
+example : b = .cons 1 .nil → h a b = 40 := by
+  unfold h
+  split
+
+
+/-
+`try?` tactic is a driver around `grind` (and other tactics).
+It tries many different things (e.g., applies function induction principle for you)
+-/
+def app : List α → List α → List α
+  | [], bs => bs
+  | a::as, bs => a :: app as bs
+
+theorem app_assoc : app as (app bs cs) = app (app as bs) cs := by
+  try?
+
+/-
+`grind` has a notion of term "generation". It is useful for avoiding
+unbounded instantiation.
+-/
+opaque bomb : Nat → Nat
+@[grind =] theorem bombEx : bomb x = bomb (bomb x) + 1 := sorry
+
+example : bomb x > 10 := by
+  grind
+
+/-
+Roadmap:
+- Improve `try?`
+- Improve diagnostics. There are so many possible improvements.
+- Improve heuristics (e.g., "weights", `grind` specific `[grind ext]`).
+- Bug fixes.
+- Linear integer arithmetic.
+- More examples like `constProp.lean`.
+- Commutative rings support (Q2).
+- Annotate standard library (Q2).
+- `grind?` argument minimization (Q2).
+- Fixing `induction a <;> grind?` (Q2).
+- `bv_decide` integration (Q2).
+- E-matching modulo associativity and commutativity?
+-/

tests/lean/grind_guide.lean.expected.out

@@ -0,0 +1,239 @@
+[grind.assert] a = 3
+[grind.assert] b = 3
+[grind.assert] ¬a = b
+[grind.eqc] f a = [1, 2]
+[grind.eqc] f b = []
+[grind.eqc] a = b
+[grind.eqc] f a = f b
+[grind.split] match x with
+    | 0 => 1
+    | n.succ => 2, generation: 0
+grind_guide.lean:60:2-60:21: error: `grind` failed
+case grind
+x : Nat
+x✝ :
+  (match x with
+    | 0 => 1
+    | n.succ => 2) =
+    0
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] (match x with
+          | 0 => 1
+          | n.succ => 2) =
+          0
+  [eqc] Equivalence classes
+    [eqc] {match x with
+        | 0 => 1
+        | n.succ => 2,
+        0}
+  [ematch] E-matching patterns
+    [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
+    [thm] _example.match_1.eq_2: [_example.match_1 #3 (Lean.Grind.offset #2 (1)) #1 #0]
+  [limits] Thresholds reached
+    [limit] maximum number of case-splits has been reached, threshold: `(splits := 0)`
+grind_guide.lean:68:2-68:7: error: `grind` failed
+case grind.1
+x : Nat
+x✝ :
+  (match x with
+    | 0 => 1
+    | n.succ => 2) ≤
+    1
+h : x = 0
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] (match x with
+          | 0 => 1
+          | n.succ => 2) ≤
+          1
+    [prop] x = 0
+    [prop] (match 0 with
+          | 0 => 1
+          | n.succ => 2) =
+          1
+  [eqc] True propositions
+    [prop] (match x with
+          | 0 => 1
+          | n.succ => 2) ≤
+          1
+    [prop] (match 0 with
+          | 0 => 1
+          | n.succ => 2) =
+          1
+  [eqc] Equivalence classes
+    [eqc] {match 0 with
+        | 0 => 1
+        | n.succ => 2,
+        match x with
+        | 0 => 1
+        | n.succ => 2,
+        1}
+    [eqc] {x, 0}
+  [cases] Case analyses
+    [cases] [2]: match x with
+        | 0 => 1
+        | n.succ => 2
+  [ematch] E-matching patterns
+    [thm] _example.match_1.eq_1: [_example.match_1 #2 `[0] #1 #0]
+    [thm] _example.match_1.eq_2: [_example.match_1 #3 (Lean.Grind.offset #2 (1)) #1 #0]
+  [offset] Assignment satisfying offset contraints
+    [assign] match x with
+        | 0 => 1
+        | n.succ => 2 := 1
+[grind] Issues
+  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] _example.match_1.eq_1 ↦ 1
+grind_guide.lean:82:19-82:21: warning: declaration uses 'sorry'
+[grind.assert] f a = b
+[grind.assert] a = g c
+[grind.assert] ¬b = c
+[grind.ematch.instance] fg: f (g c) = c
+[grind.assert] f (g c) = c
+grind_guide.lean:100:19-100:25: warning: declaration uses 'sorry'
+grind_guide.lean:101:19-101:24: warning: declaration uses 'sorry'
+[grind.assert] R a b
+[grind.assert] R c b
+[grind.assert] R d c
+[grind.assert] ¬R a d
+[grind.assert] R a d → R d a
+[grind.assert] R d c → R c d
+[grind.assert] R c b → R b c
+[grind.assert] R a b → R b a
+[grind.assert] R a d → R d c → R a c
+[grind.assert] R d c → R c b → R d b
+[grind.assert] R d b → R b d
+[grind.assert] R a c → R c a
+[grind.assert] R b a → R a b
+[grind.assert] R b c → R c b
+[grind.assert] R c d → R d c
+[grind.assert] R d a → R a d
+[grind.assert] R d b → R b c → R d c
+[grind.assert] R d b → R b a → R d a
+grind_guide.lean:114:8-114:14: warning: declaration uses 'sorry'
+[grind.assert] bla a = b
+[grind.assert] ¬bla b = b
+[grind.assert] bla (bla a) = bla a
+grind_guide.lean:137:20-137:30: warning: declaration uses 'sorry'
+grind_guide.lean:144:2-144:12: error: `grind` failed
+case grind
+a b c d : Nat
+a✝² : R a b
+a✝¹ : R c b
+a✝ : R d c
+x✝ : ¬R a d
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] R a b
+    [prop] R c b
+    [prop] R d c
+    [prop] ¬R a d
+  [eqc] True propositions
+    [prop] R a b
+    [prop] R c b
+    [prop] R d c
+  [eqc] False propositions
+    [prop] R a d
+Try this: grind only [→ Rtrans, → Rsymm]
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] Array.get_set_ne ↦ 3
+    [thm] Array.size_set ↦ 3
+[diag] Diagnostics
+  [reduction] unfolded declarations (max: 76, num: 3):
+    [reduction] getElem ↦ 76
+    [reduction] LT.lt ↦ 47
+    [reduction] Nat.lt ↦ 35
+  [reduction] unfolded instances (max: 38, num: 1):
+    [reduction] Array.instGetElemNatLtSize ↦ 38
+  [reduction] unfolded reducible declarations (max: 351, num: 7):
+    [reduction] Array.size ↦ 351
+    [reduction] Array.toList ↦ 212
+    [reduction] outParam ↦ 172
+    [reduction] Ne ↦ 60
+    [reduction] GT.gt ↦ 46
+    [reduction] autoParam ↦ 39
+    [reduction] List.casesOn ↦ 24
+  [kernel] unfolded declarations (max: 106, num: 5):
+    [kernel] LT.lt ↦ 106
+    [kernel] outParam ↦ 46
+    [kernel] Array.size ↦ 36
+    [kernel] Array.toList ↦ 31
+    [kernel] autoParam ↦ 26
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+grind_guide.lean:266:43-268:7: error: unsolved goals
+case h_1
+b a : Vec Nat (0 + 1)
+n✝¹ : Nat
+v✝ w✝ : Vec Nat n✝¹
+n✝ : Nat
+x✝ : Vec Nat (n✝ + 1 + 1)
+a✝² a✝¹ : Nat
+a✝ : Vec Nat n✝
+heq✝² : 0 + 1 = n✝ + 1 + 1
+heq✝¹ : HEq a x✝
+heq✝ : HEq b (Vec.cons a✝² (Vec.cons a✝¹ a✝))
+⊢ b = Vec.cons 1 Vec.nil → 20 = 40
+
+case h_2
+b a : Vec Nat (0 + 1)
+n✝ : Nat
+v✝ w✝ : Vec Nat n✝
+x✝ : Vec Nat 0
+heq✝² : 0 + 1 = 0
+heq✝¹ : HEq a Vec.nil
+heq✝ : HEq b x✝
+⊢ b = Vec.cons 1 Vec.nil → 30 = 40
+
+case h_3
+n✝ : Nat
+v✝¹ w✝¹ : Vec Nat n✝
+v✝ w✝ : Vec Nat (0 + 1)
+x✝¹ :
+  ∀ (n : Nat) (x : Vec Nat (n + 1 + 1)) (a a_1 : Nat) (a_2 : Vec Nat n),
+    0 + 1 = n + 1 + 1 → HEq v✝ x → HEq w✝ (Vec.cons a (Vec.cons a_1 a_2)) → False
+x✝ : ∀ (x : Vec Nat 0), 0 + 1 = 0 → HEq v✝ Vec.nil → HEq w✝ x → False
+⊢ w✝ = Vec.cons 1 Vec.nil → 40 = 40
+Try this: (induction as, bs using app.induct) <;> grind? [= app]
+grind_guide.lean:287:19-287:25: warning: declaration uses 'sorry'
+grind_guide.lean:290:2-290:7: error: `grind` failed
+case grind
+x : Nat
+x✝ : bomb x ≤ 10
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] bomb x ≤ 10
+    [prop] bomb x = bomb (bomb x) + 1
+    [prop] bomb (bomb x) = bomb (bomb (bomb x)) + 1
+    [prop] bomb (bomb (bomb x)) = bomb (bomb (bomb (bomb x))) + 1
+    [prop] bomb (bomb (bomb (bomb x))) = bomb (bomb (bomb (bomb (bomb x)))) + 1
+    [prop] bomb (bomb (bomb (bomb (bomb x)))) = bomb (bomb (bomb (bomb (bomb (bomb x))))) + 1
+  [eqc] True propositions
+    [prop] bomb x ≤ 10
+  [eqc] Equivalence classes
+    [eqc] {bomb (bomb (bomb (bomb (bomb x)))), bomb (bomb (bomb (bomb (bomb (bomb x))))) + 1}
+    [eqc] {bomb (bomb (bomb (bomb x))), bomb (bomb (bomb (bomb (bomb x)))) + 1}
+    [eqc] {bomb (bomb (bomb x)), bomb (bomb (bomb (bomb x))) + 1}
+    [eqc] {bomb (bomb x), bomb (bomb (bomb x)) + 1}
+    [eqc] {bomb x, bomb (bomb x) + 1}
+  [ematch] E-matching patterns
+    [thm] bombEx: [bomb #0]
+  [offset] Assignment satisfying offset contraints
+    [assign] bomb x := 5
+    [assign] bomb (bomb x) := 4
+    [assign] bomb (bomb (bomb x)) := 3
+    [assign] bomb (bomb (bomb (bomb x))) := 2
+    [assign] bomb (bomb (bomb (bomb (bomb x)))) := 1
+    [assign] bomb (bomb (bomb (bomb (bomb (bomb x))))) := 0
+  [limits] Thresholds reached
+    [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`
+    [limit] maximum term generation has been reached, threshold: `(gen := 5)`
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] bombEx ↦ 5