# Zulip Chat Archive

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

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