## 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 }.