INduction_

Stream: new members

[Alistair Tucker]

Hello again! I'm still having a little trouble with my induction. In the example below the second dite gives me

term
  λ (h : card s ≠ n), sol.v s _
has type
  Π (h : card s ≠ n) (y : α), y ∈ sol.V s _ → β
but is expected to have type
  ¬card s = n → Π (y : α), y ∈ V s hs → β

But by the definition, V s hs should be the same as sol.V s (lt_of_ne s hs h)?

import data.finset
open nat finset

def names : finset string := {"BARC", "HSBC", "LLOY", "NATW", "RBSG", "SANT", "STDCH"}
def B : Type := {s : string // s ∈ names}

structure soln (α β : Type) (n : nat) :=
(V : Π (s : finset B), card s < n → set α)
(v : Π (s : finset B) (hs : card s < n) (y : α), y ∈ V s hs → β)

variable {find_domain (α β : Type) (n : nat) (s : finset B) : card s = n → soln α β n → set α}
variable {solve_pde (α β : Type) (n : nat) (s : finset B) : card s = n → soln α β n → Π (V : set α) (y : α), y ∈ V → β}

def solve_system {α β : Type} : Π (n : nat), soln α β n :=
nat.rec
    (let V (s : finset B) (hs : card s < 0) : set α := false.elim (not_lt_zero (card s) hs) in
        let v (s : finset B) (hs : card s < 0) : Π (y : α), y ∈ V s hs → β := false.elim (not_lt_zero (card s) hs) in
        @soln.mk α β 0 V v)
    (λ (n : nat) (sol : soln α β n),
        let lt_of_ne (s : finset B) (hs : card s < succ n) : card s ≠ n → card s < n :=
            have h1 : card s < n ∨ card s = n, from lt_succ_iff_lt_or_eq.mp hs,
            assume h2 : card s ≠ n, or.elim h1 id (λ h, absurd h h2) in
        let V (s : finset B) (hs : card s < succ n) : set α :=
            dite (card s = n)
                (λ (h : card s = n), find_domain α β n s h sol)
                (λ (h : card s ≠ n), sol.V s (lt_of_ne s hs h)) in
        let v (s : finset B) (hs : card s < succ n) : Π (y : α), y ∈ V s hs → β :=
            dite (card s = n)
                (λ (h : card s = n), solve_pde α β n s h sol (V s hs))
                (λ (h : card s ≠ n), sol.v s (lt_of_ne s hs h)) in
        @soln.mk α β (succ n) V v)

[Alistair Tucker]

As you can probably tell by the names, I am attempting some applied mathematics :)

[Reid Barton]

V s hs isn't equal to sol.V s (lt_of_ne s hs h) in general, only when you have the hypothesis ¬card s = n, and even then it's not a definitional equality. You have to use dif_neg to simplify the dite.

[Reid Barton]

I haven't looked carefully at what's going on here, but I wonder if there might be an easier way--it looks like you're constructing a "solution for all sets of size < n" by induction on n, where we just pass to the inductive hypothesis if the set is not of the new size--then why not just define a "solution for all sets of size = n", and then if you want to reproduce the type of soln, just provide n = card s

[Alistair Tucker]

Thanks! I have applied dif_neg but the final step eludes me...

let v (s : finset B) (hs : card s < succ n) : Π (y : α), y ∈ V s hs → β :=
    dite (card s = n)
        (λ (h : card s = n), solve_pde α β n s h sol (V s hs))
        (λ (h : card s ≠ n),
            have V s hs = sol.V s (lt_of_ne s hs h), from dif_neg h,
            sol.v s (lt_of_ne s hs h)) in

[Alistair Tucker]

Your description of my intended algorithm is spot on. The reason I am trying to accumulate the Vs and vs in each successive soln is so that I can prove certain relations between them.

[Reid Barton]

Now there are two ways to proceed

[Reid Barton]

The easier way is to change the last line to something like by rw this; exact sol.v s (lt_of_ne s hs h), or the term-mode equivalent using eq.rec

[Alistair Tucker]

Got it! Thank you.

[Reid Barton]

The slightly more complicated way is to instead use the equality this to turn the hypothesis y ∈ V s hs into a proof of y ∈ sol.V s _--this will probably make things easier later if you want to prove things about the values of v, because the actual β value won't be wrapped inside a rw/eq.rec

[Alistair Tucker]

I have been fortunate enough to come across this code of @Reid Barton https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/logic/crec.lean. Reckon it might be the missing link I need to make progress on my original goal from the top of this thread. (At the same time it was perhaps a little unfortunate that the first thing I ever tried to do in Lean required such trickery :slight_smile:)

[Alistair Tucker]

Is it likely to get into mathlib any time soon?

[Johan Commelin]

My guess: if you ask Reid he won't mind if you just copy and use his code. I don't think he is planning to PR it to mathlib soon (i.e. within a month).

[Patrick Thomas]

Did two different threads get mixed together by Zulip here?

[Patrick Massot]

Zulip doesn't mix threads. But users often do...

[Patrick Thomas]

The one Mario posted a bit earlier. He labeled it "without tactics".

[Patrick Thomas]

I have to leave. I will try to clarify tomorrow. Sorry.

[Alistair Tucker]

Yes it looks as if they got mixed together because they have the same name, even though mine has some extra capitals...

[Alistair Tucker]

I've proved a lemma, but I'm sure I'm making it far too complicated :(
https://gist.github.com/agjftucker/193bcb9f8b77a2bb12f06646df892208

[Alistair Tucker]

finite.exists_maximal_wrt is a bit strange to work with I think. Was it designed with some particular purpose in mind?

[Alistair Tucker]

This one: https://github.com/leanprover-community/mathlib/blob/fbce6e4d46fb22ff4145c0e854d3966ef69a983d/src/data/set/finite.lean#L410

[Alistair Tucker]

I have run into decidability issues with finite sets anyway that I resolved by using finsets in those places. Maybe it's best just to use finsets everywhere? I'm not sure what the trade-offs are

[Kenny Lau]

finite.exists_maximal_wrt is a bit strange to work with I think. Was it designed with some particular purpose in mind?

it's zorn's lemma

[Alistair Tucker]

I did come across a file called zorn but that seemed a bit more general. And the two seem to have been written independently. In the finite case maybe it can be proved without choice? or something

[Kenny Lau]

in the finite case you automatically have the chain condition

[Kevin Buzzard]

@Alistair Tucker

apply and.intro -- you can just write split. But you can just make the entire term without too much trouble: instead of

    apply and.intro, -- `split`
    { exact subset.trans (and.left h₁) (and.left hr), },
    { exact and.right h₁, }, },

you can just write exact ⟨subset.trans h₁.1 hr.1, h₁.2⟩},. Similarly apply and.intro (and.left h₁), could just be split, exact h₁.1,.