## Stream: new members

### Topic: INduction_

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


#### Alistair Tucker (Sep 25 2018 at 07:30):

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

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

#### 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

#### 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


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

#### Reid Barton (Sep 25 2018 at 12:27):

Now there are two ways to proceed

#### 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

#### Alistair Tucker (Sep 25 2018 at 12:44):

Got it! Thank you.

#### 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

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

#### Alistair Tucker (Apr 27 2019 at 07:04):

Is it likely to get into mathlib any time soon?

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

#### Patrick Thomas (Apr 27 2019 at 20:50):

Did two different threads get mixed together by Zulip here?

#### Patrick Massot (Apr 27 2019 at 20:53):

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

#### Patrick Thomas (Apr 27 2019 at 21:49):

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

#### Patrick Thomas (Apr 27 2019 at 22:12):

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

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

#### 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

#### 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?

#### 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

#### 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

#### 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

#### Kenny Lau (Jun 26 2019 at 01:03):

in the finite case you automatically have the chain condition

#### 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