Help with proofs

Stream: new members

[Simon Daniel]

I have a structure Type that represents an existing key of an AssocList. Lean is smart enough to automatically "convert" the type to other lists where the key is present aswell. It can figure out, that if replace any key-value pair, the resulting list will still contain the key. However when choosing the replaced key to be arbitrary lean fails to do so which confuses me

structure contained_elem (l: Lean.AssocList Nat Unit) where
  n: Nat
  p: (l.find? n).isSome := by decide

def test_list: Lean.AssocList Nat Unit := [(3, ())].toAssocList'
def ce: contained_elem test_list := contained_elem.mk 3

variable (x:Nat)

def ce2: contained_elem (test_list.replace 3 ()) := ce -- conversion works magically
def ce3: contained_elem (test_list.replace x ()) := ce -- conversion does not work

def test_fun {ls: Lean.AssocList Nat Unit}: contained_elem ls -> Unit
| ce =>
  let other_l: contained_elem (ls.replace 4 ()) := ce -- also does not work
  ()

[Bolton Bailey]

This seems like a sensible error to me. In the definition of ce2 you replace the element with the same element so the Assoclist is the same, so it is fine that ce is used as a contained_elem of that list, that type checks. But if x is different from 3, the list may not be the same so it is not permissible to use ce as an contained_elem of that list, because the type of ce is only known to be contained_elem test_list, not contained_elem (test_list.replace x ())

[Bolton Bailey]

I guess your point is test_list.replace x () will always be equal to test_list no matter what x is. But that is a fact that needs proof.

[Simon Daniel]

Bolton Bailey said:

I guess your point is test_list.replace x () will always be equal to test_list no matter what x is. But that is a fact that needs proof.

thats it, i tried to prove it with simp? and exact?, but those cannot close the goal (which i thought they should be able to)

also my example works for any chosen Nat, not only 3

def ce2: contained_elem (test_list.replace 666 ()) := ce -- doesnt touch key 3 and works

[Bolton Bailey]

also my example works for any chosen Nat not only 3

Yes, I see that now. But my confusion was the same as Lean's in this instance. I was not aware of the exact definition of replace so I didn't know if the types would be equal. It seems like a case of the difference between propositional and definitional equality.

Seems like filling in the sorry below is what you want to do

def ce3: contained_elem (test_list.replace x ()) :=
  cast
  (by
    congr
    by_cases h : x = 3
    · rw [h]
      rfl
    ·
      sorry
  ) ce -- conversion does not work