Twins in context

Stream: general

[deepest recursion]

Hi. I am writing some lean an have few things in context which include these

q : quo T f
fid : f = id
⊢ HEq q quo_id

When I do rw [fid] at q, the context becomes this

q✝ : quo T f
  q : quo T id
  fid : f = id
  ⊢ HEq q✝ quo_id

Why does lean create shadowed metavariable here?

[Yaël Dillies]

That's because quo T f is a type (at least I assume. You didn't provide a #mwe so I can't actually tell), so rw doesn't remove the q with the previous type in case it was necessary for the goal to typecheck

[deepest recursion]

There are a few lines, but here it is

inductive sigmaprop (T:Type _)(P:T -> Prop) : Type _
| mksprop : (t:T) -> P t -> sigmaprop T P

def iscontr : Type _ -> Type _ := fun T => sigmaprop T (fun cc => (i:T) -> i = cc)

notation "~(" L "," R ")" => ⟨ L , R ⟩

def min_ps {P:T->Prop} : iscontr T -> (∀ i , P i) = (∃ i , P i) := by
  intro cp
  let (.mksprop cc cp) := cp
  let to : ((i:T) -> P i) -> (∃ i , P i) := fun f => ~( cc , f cc )
  let from_ : (∃ i , P i) -> (i:T) -> P i := fun ~( v2 , p ) k => by
    let eq : v2 = cc := cp v2
    let eq1 : k = cc := cp k
    let eq2 : k = v2 := by
      rw [eq]
      rw [eq1]
    rw [eq2]
    exact p
  exact Eq.propIntro to from_

def cntr_funsp : iscontr T -> iscontr (T -> T) := by
  intro cp
  let (.mksprop cc cp) := cp
  unfold iscontr
  exact (.mksprop id fun f => by
    funext k
    rw [cp k]
    simp
    generalize (f cc) = v
    rw [cp v]
  )

def no_autos : iscontr T -> {f : T -> T} -> f = id := by
  intros cp f
  let (.mksprop cc cf) := cp
  let ex : ∃ (f : T -> T) , f cc = cc := ~(id , by simp)
  funext k
  rw [cf k]
  simp
  let ac : ∀ (f : T -> T) , f cc = cc := by
    rw [min_ps (cntr_funsp cp)]
    exact ex
  exact (ac _)

def quo : (T:Type _) -> (T -> T) -> Type _ := fun T cf =>
  ∀ a:T , sigmaprop T fun i => cf a = i


def quo_id {T}: quo T id := fun i => .mksprop i rfl

def quo_contr_h1 {f}: iscontr T -> {q:quo T f} -> HEq q (@quo_id T) := by
  intros p q
  let (.mksprop cc cp) := p
  let fid := no_autos (f:=f) p

  -- rw [fid] at q -- WHY??

  admit

[deepest recursion]

I didn't hide it behind the spoiler cus it ruins the layout

[Yaël Dillies]

Okay so you can just subst fid and everything will work fine

[deepest recursion]

Hmm, how did you know what to do here?

[Yaël Dillies]

f is a free variable, so you can just substitute it

[Yaël Dillies]

In general, if you have HEq in your goal then you need to give up on rw and start using subst instead

[deepest recursion]

I think lean is doing it again...

def iterf : Nat -> (T -> T) -> (T -> T)
| .zero , _ => id
| .succ (.zero), f => fun i => f i
| .succ (.succ a), f => fun i => ((iterf (.succ a) f) (f i))

def orbit : T -> (T -> T) -> Type _ := fun is f =>
  sigmaprop Nat fun k => (iterf k f is) = is

def id_orbit : orbit a id := .mksprop 0 rfl

def id_orbit_contr : iscontr (orbit a id) := .mksprop id_orbit fun i => by
  let (.mksprop t k) := i
  induction t

  -- unfold iterf at k;

It shadows k for some reason. Can't figure out what causes this behaviour :(

[deepest recursion]

Hmm, it seems like rw can't handle an expression under lambda. Is there a workaround?

def id_iter {T}: ∀ a , (iterf a (@id T)) = id := fun i => by
  induction i
  unfold iterf
  rfl
  case succ n ih =>
    cases n
    rfl
    unfold iterf;
    simp
    rw [ih]

def id_iter2 : ∀ a b , (iterf a (@id T)) = (iterf b id) := by
  intro a b
  rw [id_iter]
  rw [id_iter]

def id_orbit_contr : iscontr (orbit a id) := .mksprop id_orbit (by
  intro i
  unfold orbit at i
  rw [id_iter2 _ 0] at i -- fails here
)

[deepest recursion]

Could you please check, @Yaël Dillies ?

[Yaël Dillies]

Use simp_rw

[deepest recursion]

It seems I don't have this tactic. Is it in some external package?

[Yaël Dillies]

file#Tactic/SimpRw

[Kim Morrison]

@recursion, it is defined in Mathlib.

[llllvvuu]

simp_rw approximately calls simp only on each item on the list, so in this case you can also do simp only [id_iter2 _ 0] at i without Mathlib

(there's also the more manual way of conv at i => congr; ext; rw [id_iter2 _ 0] but the precision is not needed this case)

[deepest recursion]

Thank you. Lean's tactics feel a bit esoteric in some places...

[deepest recursion]

Hmm, I did simp only but it twined again. I also had the expectation that k would be forced to become zero, but it wasnt... Is this the expected behaviour?

[llllvvuu]

This is known as "DTT hell". https://lean-lang.org/functional_programming_in_lean/dependent-types/pitfalls.html

[llllvvuu]

FYI your sigmaprop is docs#Subtype. Rather than subtype you could consider working with docs#Set which is ~the type of subtypes and has better API