Skip to content

Commit d097609

Browse files
FWuermseFWuermse
committed
chore: cleanup
1 parent d5d5a0b commit d097609

File tree

7 files changed

+69
-76
lines changed

7 files changed

+69
-76
lines changed

‎Grw/ProofSearch.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,6 @@ partial def dfs (goals : List MVarId) (hintDB : DiscrTree (Name × Nat)) (proofR
138138
let res ← dfs (subgoals ++ rest) hintDB proofRel
139139
if res.isEmpty || (← tryClose res) then
140140
return res
141-
s ← saveState
142141
let hintEntries ← hintDB.getMatch goalType
143142
let hintEntries := hintEntries.insertionSort fun (_, p1) (_, p2) => p1 > p2
144143
let (names, prios) := hintEntries.unzip
@@ -149,7 +148,8 @@ partial def dfs (goals : List MVarId) (hintDB : DiscrTree (Name × Nat)) (proofR
149148
let res ← dfs (subgoals ++ rest) hintDB proofRel
150149
if res.isEmpty || (← tryClose res) then
151150
return res
152-
s.restore
151+
if !(← goal.isAssignedOrDelayedAssigned) then
152+
s.restore
153153
return goals
154154

155155
def search (Ψ : List MVarId) (prf : Expr) (proofRel : Expr) (d : Option LocalDecl) : TacticM Unit := do
@@ -169,6 +169,7 @@ def search (Ψ : List MVarId) (prf : Expr) (proofRel : Expr) (d : Option LocalDe
169169
-- Check other APIs to preserve sequence (may me part of the Hypotheses APIs)
170170
let goal ← goal.tryClear d.fvarId
171171
replaceMainGoal [goal]
172+
logInfo "right-to-left RW!"
172173
else
173174
let goal ← getMainGoal
174175
let mut subgoals ← goal.apply (← instantiateMVars prf)

‎Grw/Tactic.lean‎

Lines changed: 34 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -55,13 +55,22 @@ private def toHypInfo (term : Expr) : MetaM HypInfo := do
5555
pure ⟨← mkAppM' term exprs, ← inferType lhs, r, lhs.isSort, lhs, rhs, subgoals.toList⟩
5656
| _ => throwError "The given rewrite hypothesis {term}:{T} must be of the form ∀ Φs, R αs t u."
5757

58+
59+
private def getRelType (r : Expr) : MetaM Expr := do
60+
match r with
61+
| .app (.const ``relation _) T => pure T
62+
| .forallE _ T (.forallE _ T' b _) _ =>
63+
if T == T' && b == .sort 0 then
64+
return T
65+
else
66+
throwError "You tried to get the type of a relation but {r} is not a relation."
67+
| _ => throwError "You tried to get the type of a relation but {r} is not a relation."
68+
5869
/--
59-
`fail` not clear right now
6070
`id` is when we don't rewrite because no subterm can't be unified (ATOM or binary APP).
6171
`success` successful subterm rewrite.
6272
-/
6373
inductive RewriteResult where
64-
| fail
6574
| id
6675
| success (r : RewriteResultInfo)
6776

@@ -160,9 +169,13 @@ partial def subterm (t : Expr) (desiredRel : Option Expr) (l2r : Bool) (depth :
160169
let (Ψ'', snd) ← subterm u desiredRel l2r (depth + 1)
161170
-- TODO: include both shadowed rels in psi
162171
if let .success res := snd then do
163-
let desiredRel := match desiredRel with
164-
| some r => r
165-
| none => rel
172+
let desiredRel ← match desiredRel with
173+
| some r => do
174+
if (← getRelType (← inferType r)) == .sort 0 then
175+
mkAppM ``flip #[mkConst ``impl]
176+
else
177+
pure r
178+
| none => pure rel
166179
let (p₁, rel, Ψ₁) ← subrelInference p rel desiredRel
167180
let (p₂, _, Ψ₂) ← subrelInference res.rewPrf res.rewCar desiredRel
168181
-- Invariant: all desired rels are Prop and transitive and res is of desired rel
@@ -199,7 +212,6 @@ partial def subterm (t : Expr) (desiredRel : Option Expr) (l2r : Bool) (depth :
199212
prfArgs := prfArgs ++ [rew.rewPrf]
200213
u := .app u rew.rewTo
201214
rewMVars := rew.rewMVars ++ rewMVars
202-
| .fail => return (Ψ, .fail)
203215
if prefixId then
204216
trace[Meta.Tactic.grewrite] "{srep depth} |APP - ALL ID {t}"
205217
return (Ψ, .id)
@@ -247,7 +259,6 @@ partial def subterm (t : Expr) (desiredRel : Option Expr) (l2r : Bool) (depth :
247259
| throwError "Rewrite of `all λ x ↦ y` resulted in a different (thus wrong) type."
248260
let u := .forallE n T b i
249261
pure (Ψ, .success ⟨S, t, u, p, subgoals⟩)
250-
| .fail => return ([], .fail)
251262
| _ => do
252263
trace[Meta.Tactic.grewrite] "{srep depth} |ATOM {t}"
253264
pure ([], .id)
@@ -297,7 +308,6 @@ def algorithm (ps : TSyntax `rewrite) : TacticM Unit := withMainContext do
297308
let (Ψ, res) ← subterm goalType desired l2r 0 ρ
298309
match res with
299310
| .id => logWarningAt stx m!"Nothing to rewrite for {name}."
300-
| .fail => logError "Rewrite failed to generate constraints."
301311
| .success ⟨r, _, _, p, _subgoals⟩ =>
302312
-- TODO: set subgoals
303313
let (p, _, Ψ') ← subrelInference p r desired
@@ -348,13 +358,14 @@ private def assertConstraints (ps : TSyntax `grw_assert) (ts : Syntax.TSepArray
348358
| none => do goal.getType
349359
| some l => do inferType l.toExpr
350360
let ρ ← toHypInfo expr
351-
let desired : Expr ← match location with
352-
| none => do mkAppM ``flip #[mkConst ``impl]
353-
| some _ => do pure <| Lean.mkConst ``impl
361+
let desired : Expr ← match (location, l2r) with
362+
| (none, true) => do mkAppM ``flip #[mkConst ``impl]
363+
| (some _, true) => do pure <| Lean.mkConst ``impl
364+
| (none, false) => do pure <| Lean.mkConst ``impl
365+
| (some _, false) => do mkAppM ``flip #[mkConst ``impl]
354366
let (Ψ, res) ← subterm goalType desired l2r 0 ρ
355367
match res with
356368
| .id => logWarningAt stx m!"Nothing to rewrite for {name}."
357-
| .fail => logError "Rewrite failed to generate constraints."
358369
| .success ⟨r, _, _, p, _subgoals⟩ =>
359370
-- TODO: set subgoals
360371
let (p, _, Ψ') ← subrelInference p r desired
@@ -367,9 +378,17 @@ private def assertConstraints (ps : TSyntax `grw_assert) (ts : Syntax.TSepArray
367378
else
368379
throwError "Constraints don't match at idx: {i}, {e} ≠ {ts.get! i}"
369380
-- Check if p can be applied
370-
let _ ← withoutModifyingState do
371-
let _ ← goal.apply p
372-
-- TODO: maybe check resulting type of first goal with some given "expected" type
381+
if let some l := location then
382+
let _ ← withoutModifyingState do
383+
let newExpr := Expr.app p l.toExpr
384+
let (_, goal) ← goal.assertHypotheses #[{userName := l.userName, type := ← inferType newExpr, value := newExpr}]
385+
-- Check other APIs to preserve sequence (may me part of the Hypotheses APIs)
386+
let goal ← goal.tryClear l.fvarId
387+
replaceMainGoal [goal]
388+
else
389+
let _ ← withoutModifyingState do
390+
let _ ← goal.apply p
391+
-- TODO: maybe check resulting type of first goal with some given "expected" type
373392

374393
elab rw:grw_assert t:term,+ ";": tactic =>
375394
assertConstraints rw t

‎GrwTest/Attribute.lean‎

Lines changed: 0 additions & 40 deletions
This file was deleted.

‎GrwTest/ConstraintGeneration/CoqConstraintComparison.lean‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
11
import Grw.Tactic
2-
import Grw.Eauto
32

43
section Examples
54

5+
/-
6+
This test compares all constraints and proofs generated by `grewrite` with the proof and constraints Coq generates for the same problems. As we do not attempt to solve constraints here, every test has a `sorry` at the end.
7+
-/
8+
69
/- Coq constraints: ✓
710
Proper (Iff ==> flip impl) (impl Q)
811
-/
@@ -306,7 +309,7 @@ example (h: Rα a a') (finish: Pα a'): Pα a ∧ Pα a ∧ Pα a ∧ Pα a ∧
306309

307310
variable {SET : Type}
308311
variable {eqset : relation SET}
309-
def trueRelation (α : Type) : relation α := fun _ _ => True
312+
def trueRelation' (α : Type) : relation α := fun _ _ => True
310313
variable {eqsetEquiv : Equiv eqset}
311314
variable {empty : SET}
312315
variable {union : SET → SET → SET}
@@ -464,38 +467,39 @@ example {r : α → α → Prop} [Equiv r] : r b a → r b c → r a c := by
464467
assert_constraints [← rab]
465468
(relation α),
466469
(ProperProxy ?r c),
467-
(Proper (r ⟹ ?r ⟹ flip impl) r);
470+
(Proper (r ⟹ ?r ⟹ impl) r);
468471
sorry
469472

470473
/- Coq constraints:
471474
Fails with invalid constraints. Only works with leibniz equality in Coq. BUT WE CAN!
472-
475+
-/
473476
variable (f : α → Prop → γ → Prop)
474477
example (h: f = g) : f a (f a (f a (f a True c) c) c ∧ True) c := by
475478
assert_constraints [h]
476479
(relation Prop),
477-
(ProperProxy ?r c),
478480
(relation γ),
481+
(ProperProxy ?r c),
479482
(relation Prop),
480483
(Proper (?r0 ⟹ ?r ⟹ ?r1) (g a)),
481484
(Subrel ?r2 (flip impl)),
482485
(Subrel ?r1 (flip impl)),
483486
(Transitive (flip impl)),
484-
(ProperProxy ?r3 c),
485487
(relation γ),
488+
(ProperProxy ?r3 c),
489+
(relation Prop),
486490
(Proper (flip impl ⟹ ?r3 ⟹ ?r4) (g a)),
487491
(Subrel ?r5 (flip impl)),
488492
(Subrel ?r4 (flip impl)),
489493
(Transitive (flip impl)),
494+
(relation Prop),
490495
(ProperProxy ?r5 True),
491496
(relation Prop),
492497
(Proper (flip impl ⟹ ?r5 ⟹ ?r6) And),
493-
(ProperProxy ?r7 c),
494498
(relation γ),
499+
(ProperProxy ?r7 c),
495500
(Proper (?r6 ⟹ ?r7 ⟹ flip impl) (g a)),
496501
(Subrel ?r8 (flip impl)),
497502
(Transitive (flip impl));
498503
sorry
499504

500-
-/
501505
end Examples

‎GrwTest/GrwTest.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
import GrwTest.ConstraintGeneration.CoqConstraintComparison
22
import GrwTest.TestsGrewrite
3-
import GrwTest.Attribute
3+
import GrwTest.SetEq

‎GrwTest/SetEq.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,3 +56,4 @@ theorem rewriteExample : setEq [1,2,3] [3,2,1] → setEq (addElem 4 [1,2,3]) (ad
5656
. sorry
5757
. sorry
5858
simp [setEq]
59+
sorry

‎GrwTest/TestsGrewrite.lean‎

Lines changed: 18 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,10 @@ section Examples
44

55
set_option trace.Meta.Tactic.grewrite true
66

7+
/-
8+
This test checks whether some of the rewrite tests I collected from Coq's test lib an other sources succeed. All tests that are still marked with `sorry` do emit the correct proofs and constraints but the proof search does not solve all constraints. The ones not containing a `sorry` work as expected.
9+
-/
10+
711
example : ∀ P Q : Prop , (P ↔ Q) → (Q → P) := by
812
intro P Q h
913
grewrite [h]
@@ -14,7 +18,7 @@ example : ∀ P Q : Prop, (P ↔ Q) → (Q → P) ∧ (Q → P) := by
1418
grewrite [h]
1519
simp
1620

17-
example {r : relation Prop} [hp : Subrel r (flip impl)] : r a b → b → a := by
21+
example {r : relation Prop} (hp : Subrelation r (flip impl)) : r a b → b → a := by
1822
intro rab hb
1923
grewrite [rab]
2024
exact hb
@@ -23,24 +27,28 @@ example {r : relation α} {P : α → Prop} [Proper (r ⟹ flip impl) P] : r a a
2327
intros h finish
2428
grewrite [h]
2529
exact finish
30+
-- TODO: missing tactics for Equiv rels in proof search
31+
sorry
2632

2733
example {f : α → α} [Proper (r ⟹ r) f] [Proper (r ⟹ flip impl) P] : r a a' → P (f a') → P (f a) := by
2834
intro h finish
2935
grewrite [h]
3036
exact finish
37+
-- TODO: missing tactics for Equiv rels in proof search
38+
repeat sorry
3139

3240
example {a : α} {P : (α → α) → Prop} [Proper (pointwiseRelation α r ⟹ flip impl) P] : r a a' → P (λ _ => a') → P (λ _ => a) := by
3341
intro h finish
3442
grewrite [h]
3543
exact finish
36-
37-
-- TODO: pi example
44+
-- TODO: missing tactics for Equiv rels in proof search
45+
sorry
3846

3947
example {r : α → α → Prop} [Equiv r] : r a b → r b c → r a c := by
4048
intro rab rbc
4149
grewrite [rab]
4250
assumption
43-
-- TODO: missing theorems for Equiv rels in proof search
51+
-- TODO: missing tactics for Equiv rels in proof search
4452
repeat sorry
4553

4654
example : ∀ P Q : Prop, (P ↔ Q) → Q ∧ (Q → Q) → Q ∧ (Q → P) := by
@@ -53,7 +61,7 @@ example : ∀ P Q : Prop, (P ↔ Q) → Q ∧ (Q → Q) → Q ∧ (P → Q) := b
5361
grewrite [H]
5462
exact finish
5563

56-
example [Subrel Iff (flip impl)] : ∀ P Q : Prop, (P ↔ Q) → Q → P := by
64+
example (_ : Subrelation Iff (flip impl)) : ∀ P Q : Prop, (P ↔ Q) → Q → P := by
5765
intros P Q H finish
5866
grewrite [H]
5967
exact finish
@@ -97,7 +105,7 @@ variable [PER Rα] [PER Rβ]
97105

98106
example (h: Rα a a') (finish: Pα a') : Pα a := by
99107
grewrite [h]
100-
-- TODO add per theorems to proof search
108+
-- TODO add per tactics to proof search
101109
exact finish
102110
sorry
103111

@@ -156,14 +164,14 @@ Proper (?r ==> ?r8 ==> Basics.flip Basics.impl) and
156164
example (h: Rα a a') (finish: Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a') : Pα a ∧ Pα a ∧ Pα a ∧ Pα a ∧ Pα a ∧ Pα a := by
157165
grewrite [h]
158166
exact finish
167+
-- Missing tactics
168+
repeat sorry
159169

160170
example : ∀ P Q : Prop, (P ↔ Q) → (Q → P) := by
161171
intros P Q H
162172
grewrite [H]
163173
simp
164174

165-
--Proof: Subrel.subrelation (impl Q) (impl Q) (Subrel.subrelation impl impl Proper.proper Q Q Proper.proper) P Q H
166-
167175
-- Examples from the Paper
168176
example : ∀ P Q : Prop, (P ↔ Q) → (Q → P) ∧ (Q → P) := by
169177
intros P Q H
@@ -196,7 +204,7 @@ Some Coq constraints for problems:
196204
-/
197205

198206
-- Produces: Subrel Iff (flip impl) ✓
199-
example (s : Subrel Iff (flip impl)) : ∀ P Q : Prop, (P ↔ Q) → Q → P := by
207+
example (s : Subrelation Iff (flip impl)) : ∀ P Q : Prop, (P ↔ Q) → Q → P := by
200208
intros P Q H HQ
201209
grewrite [H]
202210
exact HQ
@@ -332,7 +340,7 @@ example : ∀ P Q : Prop, (P ↔ Q) → (Q → Q) ∧ (Q → P) := by
332340
apply And.intro <;> simp
333341

334342
-- No rewrite possible on first two proofs.
335-
example (r₁ : relation Prop) (r₂ : relation Prop) (s : Subrel r₁ (flip impl)) (h₁ : r₁ P Q) (h₂ : r₂ P Q) (H : Prop) (h₃ : r₁ H P) (finish: Q) : H := by
343+
example (r₁ : relation Prop) (r₂ : relation Prop) (s : Subrelation r₁ (flip impl)) (h₁ : r₁ Q P) (h₂ : r₂ P Q) (H : Prop) (h₃ : r₁ H P) (finish: P) : H := by
336344
-- show error only on h₁ and h₂
337345
grewrite [h₁, ← h₂, h₃]
338346
exact finish

0 commit comments

Comments
 (0)