Zulip Chat Archive

Stream: new members

Topic: Well founded recursion


view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 07:06):

Can you share a #mwe ?

view this post on Zulip 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

view this post on Zulip 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 }.

view this post on Zulip Scott Morrison (Jun 01 2020 at 12:01):

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

view this post on Zulip 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