# Zulip Chat Archive

## Stream: new members

### Topic: Well founded recursion

#### Fox Thomson (May 31 2020 at 19:32):

I'm currently trying to formalize things about impartial games and am having trouble using well founded recursion. I have defined a `subsequent`

relation similar to the ones on `pgame`

in mathlib and have shown it is well founded. To use it I have been showing that the appropriate things are subsequent and then writing `using_well_founded {dec_tac := tactic.assumption}`

. This has worked in a couple of proofs but has broken when I tried to show that P-positions (second player has a winning strategy) are not N-positions (first player has a winning strategy):

```
lemma p_imp_not_n : ∀ (G : pimpartial), p_position G → ¬ (n_position G)
| (mk 0 M) :=
begin
intro hpG,
rw zero_unique,
exact zero_not_n_position
end
| (mk (nat.succ n) M) :=
begin
intro hpG,
intro hnG,
unfold p_position at hpG,
unfold n_position at hnG,
cases hnG with i hnG',
have hpG' := hpG i,
cases hpG' with j hpG'',
have hnG'' := hnG' j,
-- For recursion
have h1 : (((mk (nat.succ n) M).move i).move j).subsequent ((mk (nat.succ n) M).move i), from subsequent.from_move ((mk (nat.succ n) M).move i) j,
have h2 : ((mk (nat.succ n) M).move i).subsequent (mk (nat.succ n) M), from subsequent.from_move (mk (nat.succ n) M) i,
have hwf : (((mk (nat.succ n) M).move i).move j).subsequent (mk n.succ M), from subsequent.from_trans (((mk n.succ M).move i).move j) ((mk n.succ M).move i) (mk n.succ M) h1 h2,
exact p_imp_not_n (((mk (nat.succ n) M).move i).move j) hpG'' hnG'',
end
using_well_founded {dec_tac := tactic.assumption}
```

This has an error saying that it could not find a well founded relation between `((mk (nat.succ n) M).move i).move j`

and `mk (nat.suc n) M`

and `hwf`

is not listed in the current state. Is there a better way to use well founded recursion and why is `hwf`

not in the current state?

#### Bryan Gin-ge Chen (Jun 01 2020 at 07:06):

Can you share a #mwe ?

#### Fox Thomson (Jun 01 2020 at 11:45):

```
universe u
inductive pimpartial : Type u
| mk : ∀ (n : ℕ), (fin n → pimpartial) → pimpartial
namespace pimpartial
-- Definitions to talk about moves
def moves : pimpartial → Type
| (mk n _) := fin n
def move : Π (G : pimpartial), G.moves → pimpartial
| (mk n M) i := M i
-- definitions of subsequent and proof it is well founded
inductive subsequent : pimpartial → pimpartial → Prop
| from_move : Π (G : pimpartial) (i : G.moves), subsequent (G.move i) G
| from_trans : Π (G H F : pimpartial), subsequent G H → subsequent H F → subsequent G F
theorem wf_subsequent : well_founded subsequent := sorry
instance : has_well_founded pimpartial :=
{ r := subsequent,
wf := wf_subsequent }
-- Definition using well founded recursion (works)
def p_position : pimpartial → Prop
| (mk 0 M) := true
| (mk (nat.succ n) M) :=
∀ (i : (mk (nat.succ n) M).moves), ∃ (j : ((mk (nat.succ n) M).move i).moves),
have hwf : (((mk (nat.succ n) M).move i).move j).subsequent (mk n.succ M), from sorry,
p_position (((mk (nat.succ n) M).move i).move j)
using_well_founded {dec_tac := tactic.assumption}
def n_position : pimpartial → Prop := sorry
-- Proof using well founded recursion (does not work)
lemma p_imp_not_n : ∀ (G : pimpartial), p_position G → ¬ (n_position G)
| (mk 0 M) := sorry
| (mk (nat.succ n) M) :=
begin
intro hpG,
intro hnG,
unfold p_position at hpG,
unfold n_position at hnG,
cases hnG with i hnG',
have hpG' := hpG i,
cases hpG' with j hpG'',
have hnG'' := hnG' j,
-- For recursion
have h1 : (((mk (nat.succ n) M).move i).move j).subsequent ((mk (nat.succ n) M).move i), from subsequent.from_move ((mk (nat.succ n) M).move i) j,
have h2 : ((mk (nat.succ n) M).move i).subsequent (mk (nat.succ n) M), from subsequent.from_move (mk (nat.succ n) M) i,
have hwf : (((mk (nat.succ n) M).move i).move j).subsequent (mk n.succ M), from subsequent.from_trans (((mk n.succ M).move i).move j) ((mk n.succ M).move i) (mk n.succ M) h1 h2,
exact p_imp_not_n (((mk (nat.succ n) M).move i).move j) hpG'' hnG'',
end
using_well_founded {dec_tac := tactic.assumption}
end pimpartial
```

#### Scott Morrison (Jun 01 2020 at 12:01):

@Fox Thomson, sorry, I don't have time to look at this now, but notice in `pgame.lean`

I used a more complicated tactic for proving well-founded-ness. Look for the line `using_well_founded { dec_tac := pgame_wf_tac }`

.

#### Scott Morrison (Jun 01 2020 at 12:01):

Not sure if that will help with your problem; I haven't read your code yet.

#### Fox Thomson (Jun 01 2020 at 20:26):

@Scott Morrison I've just tried using the tactic and it seems to be working now, thank you.

Last updated: May 10 2021 at 00:31 UTC