Verifying solution of a large system of linear equations

Stream: general

[Toby Cathcart Burn]

I'd appreciate some advice on how I should convince Lean that a system of 3787 linear equations has exactly one particular solution.
The linear equations come from the following theorems:

noncomputable def vol := MeasureTheory.volume ∘ getTiles

theorem vol_cors (ps : List Piece) : vol ps =
    vol (canon_cor_rot Cor.bl ps) / 4 +
    vol (canon_cor_rot Cor.br ps) / 4 +
    vol (canon_cor_rot Cor.tl ps) / 4 +
    vol (canon_cor_rot Cor.tr ps) / 4 := by
    rw [vol,Function.comp_apply]
    nth_rw 1 [vol_corners_sorted]
    simp

theorem vol_full' : vol [Piece.fullPiece] = 1 := by
  simp [getTiles,getTile,vol_usq,vol]

theorem vol_empty' : vol [] = 0 := by
  simp [getTiles,getTile,vol]

And in around a minute, Lean can verify that

def init : List (List Piece) :=
  (List.finRange 7).flatMap
    (fun i => (List.finRange 4).map
      (fun j => [Piece.treePiece i j 0]))

def all_pieces_needed_by (xss : List (List Piece)) : List (List Piece) :=
  (List.mergeSort (xss ++ xss.flatMap
    (fun xs => List.map (fun r => canon_cor_rot r xs)
                        [Cor.bl,Cor.br,Cor.tl,Cor.tr]))
     (· ≤ · )).dedup

def plist : List (List Piece) := Nat.iterate all_pieces_needed_by 17 (init)

theorem plist_contains_all : plist = all_pieces_needed_by plist := by
  -- decide -- After unfolding the instance 'instDecidableEqList', reduction got stuck at the 'Decidable' instance
            -- plist.hasDecEq (all_pieces_needed_by plist)
  native_decide

#eval (plist.length) -- 3785

This means we have a finite system of linear equations and some Python code tells me that it has a unique solution. I can provide this solution as a list of rational numbers.
I would like to know how to get a proof of

theorem init_vols : init.map vol = [105187607728740402443028874590589271175727417984243041331444253942248364837950737123031018215335541841177518/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 6414096097425050620500764171446769897743493331559233629508200333423987240533524436757176775373463909744921363/14040198496569921098110450890605625160855820057203888770200008143743666723979734760755150490956943003574529488, 1176698522459228389099830819267655834622649884875353804796033584561545681626359435628767068906115966430851873/3510049624142480274527612722651406290213955014300972192550002035935916680994933690188787622739235750893632372, 0, 42284834655695127325062859536576439763737670748317991543196353411630489597197835666648107752420706453507719884/74588554513027705833711770356342383667046544053895659091687543263638229471142340916511736983208759706489687905, 736343266571063881623570783362816978314866472318007127181049860729231335817598303978994808300953469180994956641/1193416872208443293339388325701478138672744704862330545467000692218211671538277454664187791731340155303835006480, 430508607342923240396615459602561656085901916611003856909524500219813256808719072877455150638297429801971077/501435660591782896361087531807343755744850716328710313221428862276559525856419098598398231819890821556233196, 420750430914961609772115498362357084702909671936972165325777015768993459351802948492124072861342167364710072/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 25612890656319030766360156938388263906837250638489325028184557498360800304211824161052872150362113755003904457/149177109026055411667423540712684767334093088107791318183375086527276458942284681833023473966417519412979375810, 323967108708429854101207238363757798575023426854071961394934730552913718188781187827099820083197152580962656077/596708436104221646669694162850739069336372352431165272733500346109105835769138727332093895865670077651917503240, 4931201186158886148615443017275731652431413483711915532303287562933183263851332100804582310589566272587491623/7020099248284960549055225445302812580427910028601944385100004071871833361989867380377575245478471501787264744, 755948091544266779327715320905298749919740212938381639470256568792552222274556487136642996044773799066141801/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 1, 1/2, 2536547679753422136345732885106290781940312914416746096203737500009855636085193105273255012857421257559598339/3510049624142480274527612722651406290213955014300972192550002035935916680994933690188787622739235750893632372, 3390303731247983503189902887825574898064532479805707071627174058253778351435298488210604791194368713480354159/3510049624142480274527612722651406290213955014300972192550002035935916680994933690188787622739235750893632372, 25612890656319030766360156938388263906837250638489325028184557498360800304211824161052872150362113755003904457/149177109026055411667423540712684767334093088107791318183375086527276458942284681833023473966417519412979375810, 323967108708429854101207238363757798575023426854071961394934730552913718188781187827099820083197152580962656077/596708436104221646669694162850739069336372352431165272733500346109105835769138727332093895865670077651917503240, 4931201186158886148615443017275731652431413483711915532303287562933183263851332100804582310589566272587491623/7020099248284960549055225445302812580427910028601944385100004071871833361989867380377575245478471501787264744, 755948091544266779327715320905298749919740212938381639470256568792552222274556487136642996044773799066141801/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 42284834655695127325062859536576439763737670748317991543196353411630489597197835666648107752420706453507719884/74588554513027705833711770356342383667046544053895659091687543263638229471142340916511736983208759706489687905, 736343266571063881623570783362816978314866472318007127181049860729231335817598303978994808300953469180994956641/1193416872208443293339388325701478138672744704862330545467000692218211671538277454664187791731340155303835006480, 430508607342923240396615459602561656085901916611003856909524500219813256808719072877455150638297429801971077/501435660591782896361087531807343755744850716328710313221428862276559525856419098598398231819890821556233196, 420750430914961609772115498362357084702909671936972165325777015768993459351802948492124072861342167364710072/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 105187607728740402443028874590589271175727417984243041331444253942248364837950737123031018215335541841177518/877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093, 6414096097425050620500764171446769897743493331559233629508200333423987240533524436757176775373463909744921363/14040198496569921098110450890605625160855820057203888770200008143743666723979734760755150490956943003574529488, 1176698522459228389099830819267655834622649884875353804796033584561545681626359435628767068906115966430851873/3510049624142480274527612722651406290213955014300972192550002035935916680994933690188787622739235750893632372, 0] := by
  sorry

(If you're interested in further details, https://penteract.github.io/pythagTree.html is the proof I'm formalizing, and https://github.com/penteract/pythagTreeProof contains my proof so far, but I hope this question is self contained without them).

[Aaron Liu]

does linarith work?

[Toby Cathcart Burn]

I'm not sure how to get to a point where it would be reasonable to apply linarith unless I generate several thousand lines of proof code to put the relevant concrete instances of vol_cors into the tactic state. Is there a way to do something like List.foldr (And.intro) (by simp:true) [plist.map vol_cors] ?

[Aaron Liu]

Not sure what you mean by that one

[Aaron Liu]

Can you get your program to output a certificate?

[Toby Cathcart Burn]

I used sympy.solvers.solveset.linsolve. I don't think that has a way to output a proof certificate. Do you know a Linear algebra solver which can do make one? (ideally one that works nicely with Lean)

[Toby Cathcart Burn]

  have  h: List.foldr (· ∧ · ) (true) (plist.map (fun ps => vol ps =
      vol (canon_cor_rot Cor.bl ps) / 4 +
      vol (canon_cor_rot Cor.br ps) / 4 +
      vol (canon_cor_rot Cor.tl ps) / 4 +
      vol (canon_cor_rot Cor.tr ps) / 4 )) := by
    sorry

almost has the type I'd need to try linarith, but I'd need to fully evaluate plist and canon_cor_rot in the type.

[Toby Cathcart Burn]

linarith doesn't work on ENNReal, so I proved the equations with vol' in place of vol

noncomputable def vol' (ps: List Piece) : ℝ  := ENNReal.toReal (vol ps)

There's something with at least quadratic runtime in the way lean parses long lists, so I split one up into 100 parts so that I could spell out the equations I need explicitly.

I've then put what should be a conjunction of all necessary equations into scope. linarith looks like it's trying to work, but it runs out of stack space.

set_option maxRecDepth 100000
set_option maxHeartbeats 200000000

theorem init_vols : List.sum (init.map vol') = 12823413011547414368862997525616691741041579688920794331363953564934456759066858494476606822552437442098640979 / 877512406035620068631903180662851572553488753575243048137500508983979170248733422547196905684808937723408093 := by
  simp [init, List.finRange]
  have  h: List.foldr (· ∧ · ) (true) (allparts2.map (fun (ps,cs) => vol' ps =
    List.sum (cs.map vol') / 4)) := by
      sorry
  have h' := vol_full'
  have h'' := vol_empty'
  simp only [allparts2,allparts, part0,
      List.map_cons, List.map_nil,
        List.flatMap_cons, List.flatMap_nil, List.append_nil, List.cons_append, List.nil_append,
        Nat.reduceDiv, List.cons.injEq, and_true] at h
  simp [part1,part2,part3,part4,part5] at h
  simp [part6,part7,part8,part9,part10] at h
  simp [part11,part12,part13,part14,part15,part16,part17,part18,part19,part20] at h
  simp [part21,part22,part23,part24,part25,part26,part27,part28,part29,part30] at h
  simp [part31,part32,part33,part34,part35,part36,part37,part38,part39,part40] at h
  simp [part41,part42,part43,part44,part45,part46,part47,part48,part49,part50] at h
  simp [part51,part52,part53,part54,part55,part56,part57,part58,part59,part60] at h
  simp [part61,part62,part63,part64,part65,part66,part67,part68,part69,part70] at h
  simp [part71,part72,part73,part74,part75,part76,part77,part78,part79,part80] at h
  simp [part81,part82,part83,part84,part85,part86,part87,part88,part89,part90] at h
  simp [part91,part92,part93,part94,part95,part96,part97,part98,part99] at h
  linarith

[Aaron Liu]

If you get a certificate you can use linear_combination instead, which takes the burden of finding a solution off Lean.

[Toby Cathcart Burn]

Thanks, that's very helpful. I hadn't realized what a proof certificate would look like until you told me about that.

I think the sum of rows of the inverse matrix of A (where Ax=b is the system of linear equations), so solving Aᵀy = v (where v describes the equation I want to verify) gives me the coefficients I need for linear_combination. I might try and find another way to use those coefficients, since the linear_combination line would have to be awkwardly long, and getting concrete statements of particular equations isn't straightforward (evaluating canon_cor_rot several thousand times doesn't seem to work unless I use native_decide).