fun with pfun and dite

Stream: new members

[Jalex Stark]

This code block is kinda long but I think is close to minimal. I'm trying to define a notion of the limit of an increasing sequence of partial functions. I define the limiting function in tactic mode using by_cases. Later I unfold it and try to tell Lean which branch it goes down with rw dif_pos, but I get an error

rewrite tactic failed, did not find instance of the pattern in the target expression
  dite ?m_1 ?m_4 ?m_5

while the goal state looks like

a ∈
    dom
      (id
         (λ (a : α),
            dite (∃ (n : ℕ), a ∈ dom (F n))
              (λ (h : ∃ (n : ℕ), a ∈ dom (F n)), let k : ℕ := classical.some h in F k a)
              (λ (h : ¬∃ (n : ℕ), a ∈ dom (F n)), ↑none)))

which to my human eyes clearly contains dite _ _ _ in it.

Here's the code:

import tactic
import data.set.basic

universes u
open_locale classical
open pfun

def pfun.extends {α β : Type} (F f : α  →. β) : Prop := dom f ⊆ dom F ∧ ∀ a ha ha', (f a).get ha = (F a).get ha'


def limit_of_chain {α β : Type}  (F : ℕ → (α →. β)) (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n) ) : α →. β := begin
intro a,
by_cases ∃ n, a ∈ dom (F n),
 swap, {exact none},
have hk := classical.some_spec h,
let k:= classical.some h,
exact (F k) a,
end

def limit_of_chain_extends {α β : Type}  (F : ℕ → (α →. β)) (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n)) : ∀ n, pfun.extends (limit_of_chain F F_chain) (F n) := begin
intro n, rw pfun.extends,
split,
    rw set.subset_def, intros a ha,
    unfold limit_of_chain,
rw dif_pos,
end

[Mario Carneiro]

it's under a binder

[Mario Carneiro]

simp can get at this, rw can't

[Jalex Stark]

oh interesting

[Jalex Stark]

so simp only [dif_pos] will make progress?
EDIT: I think it doesn't

[Reid Barton]

Perhaps we could improve the error message

[Kenny Lau]

should we rewrite rw so that it can access binders?

[Reid Barton]

I mean, there is a lot that can go wrong with rw, but in this case the error message is actually just a lie

[Mario Carneiro]

there is simp_rw I think, which uses simp with settings to make it act more like rw

[Kenny Lau]

but can it succeed without knowing all the inputs of a theorem?

[Kenny Lau]

because rw can (and generates metavariables) while simp fails

[Jalex Stark]

in my context, simp only [id.def, roption.coe_none], and simp_rw dif_pos, have the same effect

[Mario Carneiro]

simp only [dif_pos] will not make progress because it doesn't have the proof of the condition available

[Mario Carneiro]

unlike rw, which is happy to apply conditional rewrites and gives you the conditions as subgoals

[Mario Carneiro]

Does simp only [dif_pos _] work?

[Jalex Stark]

have calc1 : ∃ (n : ℕ), a ∈ dom (F n), use n, exact ha, simp only [dif_pos, calc1],
this doesn't work

[Jalex Stark]

neither does simp only [dif_pos _]

[Jalex Stark]

(would these problems not arise if I was avoiding the use of tactics in constructing data?)

[Reid Barton]

The binder binds a different a. Actually I can't tell what is happening.

[Jalex Stark]

Reid Barton said:

The binder binds a different a. Actually I can't tell what is happening.

does simp only [id.def, roption.coe_none], make it a little clearer?

[Reid Barton]

Oh right, a pfun actually is a function. Maybe it would be more profitable to simplify from the outside first.

[Reid Barton]

Like presumably a \in dom f is some assertion about f a, and then the lambda will reduce

[Reid Barton]

and then you wouldn't be in this situation where you can't provide the proof of which case you are in because you have no way to talk about the variable a

[Jalex Stark]

I think maybe this did some "simplifying from the outside" although I'm not really sure what happened (the work_on_goal line came from tidy?)

import tactic
import data.set.basic

universes u
open_locale classical
open pfun

def pfun.extends {α β : Type} (F f : α  →. β) : Prop := dom f ⊆ dom F ∧ ∀ a ha ha', (f a).get ha = (F a).get ha'


def limit_of_chain {α β : Type}  (F : ℕ → (α →. β)) (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n) ) : α →. β := begin
intro a,
by_cases ∃ n, a ∈ dom (F n),
 swap, {exact none},
have hk := classical.some_spec h,
let k:= classical.some h,
exact (F k) a,
end

def limit_of_chain_extends {α β : Type}  (F : ℕ → (α →. β)) (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n)) : ∀ n, pfun.extends (limit_of_chain F F_chain) (F n) := begin
intro n, rw pfun.extends,
split,
    rw set.subset_def, intros a ha,
    unfold limit_of_chain,
-- have calc1 : ∃ (n : ℕ), a ∈ dom (F n), use n, exact ha,
simp only [id.def, roption.coe_none],

refine (mem_dom
   (λ (a : α),
      dite (∃ (n : ℕ), a ∈ dom (F n)) (λ (h : ∃ (n : ℕ), a ∈ dom (F n)), F (classical.some h) a)
        (λ (h : ¬∃ (n : ℕ), a ∈ dom (F n)), roption.none))
   a).mpr
  _,
existsi ((F n) a).get ha,
work_on_goal 0 { dsimp at *, fsplit },
rw dif_pos,
end

[Reid Barton]

By the way, part of the point of pfun is you don't have to use by_cases at all

[Jalex Stark]

hmm how would you define limit_of_chain?

[Jalex Stark]

(for my application to categoriticity of DLOs, I only need the case where the limit of the partial functions is total, so I could cut out my use of by_cases by adding the positive case as an assumption)

[Jalex Stark]

(as a zulip meta question, does this conversation belong in "new members" or "math"?)

[Reid Barton]

for example

def limit_of_chain {α β : Type} (F : ℕ → (α →. β))
  (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n) ) :
  α →. β :=
begin
  refine λ a, ⟨∃ n, a ∈ dom (F n), λ h, _⟩,
  have hk := classical.some_spec h,
  let k:= classical.some h,
  exact ((F k) a).get hk,
end

(by the way you seem to be missing noncomputable theory?)

[Reid Barton]

in principle you could make the value part computable too, since you only have to search over naturals

[Jalex Stark]

thanks, I added noncomputable theory. I should probably convince VSCode to autogenerate headers for me

[Jalex Stark]

oh cool I like this

[Jalex Stark]

with your definition, tidy can make a lot of progress :)

[Jalex Stark]

It works!

import tactic
import data.set.basic

universes u
open_locale classical
noncomputable theory
open pfun

def pfun.extends {α β : Type} (F f : α  →. β) : Prop := dom f ⊆ dom F ∧ ∀ a ha ha', (f a).get ha = (F a).get ha'

def limit_of_chain {α β : Type} (F : ℕ → (α →. β))
  (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n) ) :
  α →. β :=
begin
  refine λ a, ⟨∃ n, a ∈ dom (F n), λ h, _⟩,
  have hk := classical.some_spec h,
  let k:= classical.some h,
  exact ((F k) a).get hk,
end

lemma chain_pointwise_constant
    {α β : Type}
    (F : ℕ → (α →. β))
    (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n) ) :
    ∀ n k a ha_n ha_k, (F k a).get ha_k  = (F n a).get ha_n :=
begin
intros,
cases le_total k n;
have calc1 := F_chain _ _ h,
try {repeat {apply calc1.right
        <|> symmetry},},
end

lemma limit_of_chain_spec
    {α β : Type}
    {a : α}
    (F : ℕ → (α →. β))
    (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n))
    (ha' : (limit_of_chain F F_chain a).dom) :
    ∃ (k : ℕ) (ha_k : (F k a).dom),
    (F k a).get ha_k
    = (limit_of_chain F F_chain a).get ha' :=
begin
unfold limit_of_chain at ha', simp only [] at ha',
cases ha' with k hk, existsi k,
existsi hk,
unfold limit_of_chain, simp only [],
apply chain_pointwise_constant _ F_chain,
end

def limit_of_chain_extends {α β : Type}  (F : ℕ → (α →. β)) (F_chain : ∀ n k, k ≤ n → pfun.extends (F k) (F n)) : ∀ n, pfun.extends (limit_of_chain F F_chain) (F n) := begin
intro n, rw pfun.extends,
split,
    {rw set.subset_def, intros a ha,
    unfold limit_of_chain, tidy},
intros a ha ha',
suffices key : ∃ k ha_k, (F k a).get ha_k = (limit_of_chain F F_chain a).get ha',
cases key with k key,
cases key with ha_k key,
rw ← key,
cases le_total k n;
apply chain_pointwise_constant _ F_chain,
apply limit_of_chain_spec,
end