## Stream: general

### Topic: bug in congr'?

#### Kevin Buzzard (Jun 27 2019 at 22:05):

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 (Jun 27 2019 at 22:09):

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.

Last updated: Dec 20 2023 at 11:08 UTC