# Zulip Chat Archive

## 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: May 09 2021 at 19:11 UTC