Well founded recursion

Stream: new members

[Fox Thomson]

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]

Can you share a #mwe ?

[Fox Thomson]

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]

@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]

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

[Fox Thomson]

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