[Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton #3308

gebner · 2020-07-07T17:10:37Z

I'm surprised we didn't have this already.

example (x y : unit) : x = y := by simp

I'm not sure if this breaks anything.

ChrisHughes24 · 2020-07-07T19:00:50Z

bors merge

I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ```

gebner · 2020-07-07T19:07:11Z

bors r-

bors · 2020-07-07T19:07:13Z

Canceled.

gebner · 2020-07-07T19:31:42Z

Ah this broke a bit more than expected. Apparently fin_cases calls norm_num on the new hypothesis, which in turn calls simp. If the new hypothesis is (i : fin 1) = 0, then simp will now rewrite it to true, and the subst call in fin_cases no longer works.

I weakened the norm_num a bit so that it is only run on the rhs, but this broke interval_cases. Tomorrow I'll try moving the norm_num call entirely to interval_cases.

robertylewis · 2020-07-08T12:01:48Z

src/tactic/fin_cases.lean

@@ -46,7 +46,8 @@ meta def fin_cases_at_aux : Π (with_list : list expr) (e : expr), tactic unit
                        (to_rhs >> conv.interactive.change (to_pexpr h))
        -- Otherwise, call `norm_num`. We let `norm_num` unfold `max` and `min`
        -- because it's helpful for the `interval_cases` tactic.
-        | _ := try $ tactic.interactive.norm_num


What if you made this norm_num1 instead of norm_num to avoid calling simp? I'm not sure if it's powerful enough for whatever norm_num is intended to do here, but maybe it is, and that would be an easier fix.

I tried this as well, but interval_cases seems to heavily rely on the simplifier. Otherwise you get goals like this:

w₂: ⊥ < 2 ⊢ ⊥ = 0 ∨ ⊥ = 1 w₂: ⊥ + 1 < 2 ⊢ ⊥ + 1 = 0 ∨ ⊥ + 1 = 1

Just to recap the issues:

fin_cases should use subst on hypotheses like i = 0

the new simp lemma simplifies those to true

however in general we want the full simplifier because of interval_cases

So, I think I've fixed this. The issue was that I've been using tactic.interactive.norm_num in the conv monad, which (in hindsight) obviously doesn't work. Then I tried conv.interactive.norm_num, which also failed because it used the simplifier from the tactic monad. After fixing conv.interactive.norm_num, the tests pass. I'm keeping my fingers crossed.

gebner · 2020-07-08T14:39:48Z

It finally builds!

bryangingechen · 2020-07-08T14:42:59Z

test/tidy.lean

-  intro1,
-  induction x,
-  refl
+  simp


Should this test be testing something about tidy in some way? @semorrison

It had been a test about chain, checking that it failed when it was meant to fail. The test has become a bad one, because now the underlying tactic is succeeding (yay!). I propose we just delete this test entirely.

@semorrison

To quote @semorrison: > It had been a test about `chain`, checking that it failed when it was > meant to fail. The test has become a bad one, because now the underlying > tactic is succeeding (yay!). I propose we just delete this test > entirely.

jcommelin · 2020-07-09T05:01:19Z

bors merge

bryangingechen · 2020-07-09T05:03:25Z

Wait, did you mean to delete the entire test file?

bors r-

bryangingechen · 2020-07-09T05:04:52Z

I think @semorrison was just suggesting to delete tidy_test_0 in test/tidy.lean

jcommelin · 2020-07-09T05:46:12Z

Ooops! I should learn to be more careful!

This reverts commit 771305d.

bryangingechen · 2020-07-09T06:10:44Z

LGTM!
bors r+

I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ``` Co-authored-by: Johan Commelin <johan@commelin.net>

bors · 2020-07-09T07:36:24Z

Pull request successfully merged into master.

Build succeeded:

…ity#3308) I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ``` Co-authored-by: Johan Commelin <johan@commelin.net>

gebner added 3 commits July 7, 2020 19:06

feat(logic/basic): add eq_iff_true_of_subsingleton

624889a

Fix linear_algebra/basis

df6d674

Make fin_cases work again on (fin 1).

89d152b

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 7, 2020

bors bot pushed a commit that referenced this pull request Jul 7, 2020

feat(logic/basic): add eq_iff_true_of_subsingleton (#3308)

8d5a005

I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ```

Fix lucas_lehmer

d1de7d7

gebner removed the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 8, 2020

robertylewis reviewed Jul 8, 2020

View reviewed changes

gebner added 2 commits July 8, 2020 15:26

Fix conv.interactive.norm_num

1b211c3

Fix tidy test.

2a96a64

gebner added the awaiting-review The author would like community review of the PR label Jul 8, 2020

bryangingechen reviewed Jul 8, 2020

View reviewed changes

Delete old test

771305d

To quote @semorrison: > It had been a test about `chain`, checking that it failed when it was > meant to fail. The test has become a bad one, because now the underlying > tactic is succeeding (yay!). I propose we just delete this test > entirely.

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 9, 2020

bryangingechen removed the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 9, 2020

jcommelin added 2 commits July 9, 2020 05:46

Revert "Delete old test"

9eeda99

This reverts commit 771305d.

Delete only 1 test

2ea20cd

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 9, 2020

bors bot pushed a commit that referenced this pull request Jul 9, 2020

feat(logic/basic): add eq_iff_true_of_subsingleton (#3308)

c06f500

I'm surprised we didn't have this already. ```lean example (x y : unit) : x = y := by simp ``` Co-authored-by: Johan Commelin <johan@commelin.net>

bors bot changed the title ~~feat(logic/basic): add eq_iff_true_of_subsingleton~~ [Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton Jul 9, 2020

bors bot closed this Jul 9, 2020

bors bot deleted the ss_elim_simp branch July 9, 2020 07:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton #3308

[Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton #3308

gebner commented Jul 7, 2020 •

edited

ChrisHughes24 commented Jul 7, 2020

gebner commented Jul 7, 2020

bors bot commented Jul 7, 2020

gebner commented Jul 7, 2020

robertylewis Jul 8, 2020

gebner Jul 8, 2020

gebner Jul 8, 2020

gebner commented Jul 8, 2020

bryangingechen Jul 8, 2020

semorrison Jul 9, 2020

jcommelin commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

jcommelin commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

bors bot commented Jul 9, 2020

[Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton #3308

[Merged by Bors] - feat(logic/basic): add eq_iff_true_of_subsingleton #3308

Conversation

gebner commented Jul 7, 2020 • edited

ChrisHughes24 commented Jul 7, 2020

gebner commented Jul 7, 2020

bors bot commented Jul 7, 2020

gebner commented Jul 7, 2020

robertylewis Jul 8, 2020

Choose a reason for hiding this comment

gebner Jul 8, 2020

Choose a reason for hiding this comment

gebner Jul 8, 2020

Choose a reason for hiding this comment

gebner commented Jul 8, 2020

bryangingechen Jul 8, 2020

Choose a reason for hiding this comment

semorrison Jul 9, 2020

Choose a reason for hiding this comment

jcommelin commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

jcommelin commented Jul 9, 2020

bryangingechen commented Jul 9, 2020

bors bot commented Jul 9, 2020

gebner commented Jul 7, 2020 •

edited