bug in congr'?

Stream: general

[Kevin Buzzard]

I have been watching the lectures by Xavier Leroy https://www.college-de-france.fr/site/xavier-leroy/course-2018-2019.htm on type theory. He defined well-founded trees via a cute inductive type and then showed how to make a variant of nat. I managed to prove it was the same as nat:

import data.equiv.basic

namespace wf

-- general well-founded trees
inductive W (L : Type) (A : L → Type) : Type
| Node : ∀ (lbl : L), (A lbl → W) → W

-- model of nat as well-founded tree with nodes labelled by bool
def nat := W bool (λ b, bool.rec empty unit b)

end wf

example : equiv nat wf.nat :=
{ to_fun := λ n, nat.rec_on n (wf.W.Node ff empty.elim) (λ d w, wf.W.Node tt $ λ _, w),
  inv_fun := λ w, wf.W.rec_on w $ λ b, bool.rec_on b (λ _ _, 0) (λ H1 H2, nat.succ (H2 ())),
  left_inv := begin
    intro n,
    induction n with d hd, refl,
    dsimp,
    congr',
  end,
  right_inv := begin
    intro w,
    induction w with b H1 H2,
    cases b,
    { dsimp,
      -- congr', -- fails
      convert rfl, -- works
      ext x,
      cases x,
    },
    { dsimp,
      congr',
      ext a,
      convert (H2 a)
    }
  end
}

I don't know if dsimp, congr' is to be avoided in general, but it's pretty useful here. I nearly use it three times, except that once it didn't work -- and I was surprised that convert rfl then did work, because I was under the impression that congr' was just an abbreviation for this.

[Kevin Buzzard]

In case anyone is trying to understand the code -- W L A is well-founded trees whose nodes each have a label (from L) and the exit edges from each node with label L form a type which is A L; the well-founded tree that each one corresponds to is given by A lbl -> W in the constructor. For example, if A lbl -> W is (λ b, bool.rec empty unit b) then we're saying that a vertex is either labelled with ff and has no children, or is labelled with tt and has exactly one; such well-founded trees are then sequences of tt followed by an ff, so this is nat by some other name.