bug in 4.6-rc1?

Stream: lean4

[Jared green]

im not sure if i found a bug. something which should have been equal somehow isn't?

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable

@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl
def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

theorem any_erase :∀ l : List b,∀ a: b -> Prop,
                     ∀ s : b,s ∈ l -> ¬ (a s) -> (List.any l a <-> List.any (List.erase l s) a) :=
  by
  intro l
  intro a
  intro s
  intro hs
  intro hnas
  induction' l with c d e
  simp
  constructor
  simp at hs
  cases' (Classical.em (c = s)) with hsc hsd
  have hed : List.erase (c :: d) s = d
  unfold List.erase
  rw [hsc]
  simp
  rw [hed]
  simp
  rw [hsc]
  intro hsd
  cases' hsd with hsdl hsdr
  by_contra
  apply hnas
  exact hsdl
  exact hsdr
  cases' hs with hsl hsr
  by_contra
  apply hsd
  rw [hsl]
  simp only [Bool.or_eq_true, List.any_eq_true]
  simp at e
  intro hl
  apply e at hsr
  have hcd : List.erase (c :: d) s = c :: List.erase d s
  nth_rewrite 1 [ List.erase]
  rw [← ne_eq] at hsd
  apply beq_false_of_ne at hsd
  rw [hsd]
  rw [hcd]
  simp
  simp at hl
  rw [← hsr]
  exact hl
  simp at hs
  cases' (Classical.em (c = s)) with hsl hsr
  have hed : List.erase (c :: d) s = d
  unfold List.erase
  rw [hsl]
  simp
  rw [hed]
  simp
  rw [ hsl]
  intro f
  intro hf
  intro haf
  right
  use f
  have hcd : List.erase (c :: d) s = c :: List.erase d s
  nth_rewrite 1 [List.erase]
  rw [← ne_eq]at hsr
  apply beq_false_of_ne at hsr
  rw [hsr]
  rw [hcd]
  rw [List.any_cons]
  cases' hs with hsc hsd
  by_contra
  apply hsr
  rw [hsc]
  apply e at hsd
  rw [List.any_cons]
  simp only [Bool.or_eq_true, List.any_eq_true]
  intro hcl
  simp at hsd
  simp
  rw [hsd]
  simp at hcl
  exact hcl
theorem property2 : ∀ n : List (List (List (Bool × normalizable α pred))),
                    ∀ g : List (List (Bool × normalizable α pred)), g ∈ n ->
                    ∀ s : List (Bool × normalizable α pred), s ∈ g ->
                    ((nToProp n -> ¬(sToProp s)) -> nToProp n -> (gToProp g <-> gToProp (g.erase s))) :=
  by
  intro n
  intro g
  intro hg
  intro s
  intro hs
  intro hns
  intro hn
  unfold gToProp
  have hnos : ¬ sToProp s
  apply hns
  exact hn
  apply any_erase at g
  apply g at hs
  apply hs at hnos
  rw [hnos]
  simp
  --should have ended with rfl here
  constructor
  intro hxs
  obtain ⟨x,hx,hsx⟩ := hxs
  use x
  constructor
  sorry
  exact hsx
  sorry

[Jared green]

im still using 4.6.0-rc1

[Damiano Testa]

There are so many errors in the code that you posted, that I do not know which one is the one that you are referring to. Can you post something that has a single issue, checking that it has only one error using the web-browser?

[Jared green]

sorry there was something i had forgotten to include. i just edited it.

[Damiano Testa]

The first error that I see is on line 74: that is I think because the syntax for have changed and now you should use := by and then indent the rest of the proof.

[Jared green]

it worked without that.

[Damiano Testa]

Ok, so, yes, this changed and I don't think that it is considered a bug.

[Jared green]

the bug i described is at the end.

[Damiano Testa]

After Lean gives an error, you should not trust what it says: can you produce an example that has a single error? Otherwise, it is not clear whether the issue arises from the previous error or not.

[Eric Wieser]

Damiano Testa said:

The first error that I see is on line 74: that is I think because the syntax for have changed and now you should use := by and then indent the rest of the proof.

Or add import Mathlib.Tactic.Have

[Jared green]

there is no error. you would get one if you place rfl where i thought it should be, and thats a problem.

[Damiano Testa]

Have you opened your code with the web-editor?

[Jared green]

i am editing it in vscode

[Kyle Miller]

I hacked your code to get it to the should have ended with rfl here line, and yes, rfl doesn't work there. You can use the congr! tactic to help debug what the difference is.

There are two BEq instances that aren't defeq. The congr! tactic shows instBEq = List.instBEqList is the difference. With pp.explicit set to true, you can see the instances better:

-- First
@instBEq (List (Prod Bool (normalizable α pred))) fun a b ↦
  propDecidable (@Eq (List (Prod Bool (normalizable α pred))) a b
-- Second
@List.instBEqList (Prod Bool (normalizable α pred))
  (@instBEqProd Bool (normalizable α pred) (@instBEq Bool fun a b ↦ instDecidableEqBool a b)
    (@instBEq (normalizable α pred) fun a b ↦ @instDecidableEqNormalizable α pred (fun a b ↦ h a b) a b))

[Kyle Miller]

That's saying that the first one comes from a Decidable instance, and the second one comes from a BEq instance for List. This is a "diamond" in the instance hierarchy.

[Kyle Miller]

Here's a workaround:

First you need these theorems somewhere:

@[ext]
theorem beq_ext {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) :
    inst1 = inst2 := by
  have ⟨beq1⟩ := inst1
  have ⟨beq2⟩ := inst2
  congr
  ext x y
  exact h x y

theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
    inst1 = inst2 := by
  ext x y
  simp only [beq_eq_decide]

Then rather than rfl, you do congr! followed by apply lawful_beq_subsingleton

[Jared green]

unknown identifier beq_eq_decide

[Kyle Miller]

You can use the search box in this documentation to find out what you need to import to use it.

[Jared green]

i already have it imported.

[Jared green]

still doesnt work.

[Jared green]

when was that theorem added? my version doesnt have it.

[Kyle Miller]

It looks like it was added ten days ago: https://mathlib-changelog.org/v4/commit/a62da66e

You can copy that theorem into your project too, or update your mathlib.

[Jared green]

how do i update mathlib?

[Kyle Miller]

In any case I just made mathlib4#11179 to improve congr! to be able to handle this situation.

It would be nice if someone could figure out what's going on with this BEq instance diamond. At least this congr! upgrade will be able to help work around these issues as they come up.

[Kyle Miller]

There are instructions here: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Ruben Van de Velde]

Is this the BEq Vs DecidableEq issue that's been filed long ago?