Zulip Chat Archive

Stream: new members

Topic: INduction_


view this post on Zulip Alistair Tucker (Sep 25 2018 at 07:30):

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)

view this post on Zulip Alistair Tucker (Sep 25 2018 at 07:30):

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

view this post on Zulip Reid Barton (Sep 25 2018 at 11:49):

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.

view this post on Zulip Reid Barton (Sep 25 2018 at 11:53):

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

view this post on Zulip Alistair Tucker (Sep 25 2018 at 12:20):

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

view this post on Zulip Alistair Tucker (Sep 25 2018 at 12:23):

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.

view this post on Zulip Reid Barton (Sep 25 2018 at 12:27):

Now there are two ways to proceed

view this post on Zulip Reid Barton (Sep 25 2018 at 12:28):

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

view this post on Zulip Alistair Tucker (Sep 25 2018 at 12:44):

Got it! Thank you.

view this post on Zulip Reid Barton (Sep 25 2018 at 12:48):

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

view this post on Zulip Alistair Tucker (Apr 27 2019 at 07:04):

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:)

view this post on Zulip Alistair Tucker (Apr 27 2019 at 07:04):

Is it likely to get into mathlib any time soon?

view this post on Zulip Johan Commelin (Apr 27 2019 at 07:20):

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).

view this post on Zulip Patrick Thomas (Apr 27 2019 at 20:50):

Did two different threads get mixed together by Zulip here?

view this post on Zulip Patrick Massot (Apr 27 2019 at 20:53):

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

view this post on Zulip Patrick Thomas (Apr 27 2019 at 21:49):

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

view this post on Zulip Patrick Thomas (Apr 27 2019 at 22:12):

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

view this post on Zulip Alistair Tucker (Apr 27 2019 at 22:25):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 00:35):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 00:38):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 00:38):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 00:55):

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

view this post on Zulip Kenny Lau (Jun 26 2019 at 00:57):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 01:02):

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

view this post on Zulip Kenny Lau (Jun 26 2019 at 01:03):

in the finite case you automatically have the chain condition

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 21:25):

@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,.


Last updated: May 12 2021 at 05:19 UTC