Zulip Chat Archive
Stream: Is there code for X?
Topic: Formalizing array manipulations
Vlad (Apr 22 2024 at 21:30):
In my programming tasks, I frequently work with arrays. Below is an example of the kind of manipulations I'm interested in performing.
The current proof for this manipulation appears cumbersome and contains gaps.
Is there a more efficient way to streamline this type of work?
Specifically, I'm wondering if using Finset.sup' is a good approach.
Also, I understand that using Fin for indexing would eliminate the need for index boundary proofs, it has the limitation of only ranging from zero. My use cases often require indexing that starts from values above zero.
As a side note, I've customized the syntax for Finset.sup and Finset.sup' for better readability. Finset.sup' is further distinguished by including the hypothesis [H] next to the arrow.
import Lean
import Mathlib.Tactic
open Lean Elab Term Meta
open Finset
open BigOperators
open Algebra
namespace BigOperators
open Std.ExtendedBinder PrettyPrinter Delaborator SubExpr
scoped syntax (name := bigmax) "⇑ " ("[" term "]" )? extBinder ", " term:67 : term
scoped macro_rules (kind := bigmax)
| `(⇑ $x:ident, $p) => `(Finset.sup Finset.univ (fun $x:ident ↦ $p))
| `(⇑ $x:ident : $t, $p) => `(Finset.sup Finset.univ (fun $x:ident : $t ↦ $p))
| `(⇑ [$hne] $x:ident : $t, $p ) => `(Finset.sup' Finset.univ $hne (fun $x:ident : $t ↦ $p))
scoped syntax (name := bigmaxin) "⇑ " extBinder " in " term ", " term:67 : term
scoped macro_rules (kind := bigmaxin)
| `(⇑ $x:ident in $s, $r) => `(Finset.sup $s (fun $x ↦ $r))
| `(⇑ $x:ident : $t in $s, $p) => `(Finset.sup $s (fun $x:ident : $t ↦ $p))
@[scoped delab app.Finset.sup] def delabFinsetSup : Delab := whenPPOption getPPNotation do
let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
guard <| f.isLambda
let ppDomain ← getPPOption getPPPiBinderTypes
let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
return (i, ← delab)
if s.isAppOfArity ``Finset.univ 2 then
let binder ←
if ppDomain then
let ty ← withNaryArg 1 delab
`(extBinder| $(.mk i):ident : $ty)
else
`(extBinder| $(.mk i):ident)
`(⇑ $binder, $body)
else
let ss ← withNaryArg 4 <| delab
`(⇑ $(.mk i):ident in $ss, $body)
end BigOperators
theorem Finset.sup'_add_const {α : Type}(s: Finset α) {H: univ.Nonempty} (f : α → ℤ) (bdd: ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a) (c : ℤ) :
(⇑[H] a: s, (f a + c) ) = (⇑[H] a: s, f a) + c
:= by
apply le_antisymm
. apply sup'_le
intros
rename_i b _
gcongr
simp_all only [univ_eq_attach, mem_attach, le_sup'_iff, true_and, Subtype.exists, exists_prop]
use b
simp_rw [le_refl, coe_mem];
trivial
. simp_all only [univ_eq_attach, le_sup'_iff, mem_attach, add_le_add_iff_right, sup'_le_iff,
forall_true_left, Subtype.forall, true_and, Subtype.exists, exists_prop]
example
(xs :Array ℤ)
(i: ℕ)
(hi1: i < xs.size)
(hi2: 0 < i)
{H: univ.Nonempty}
: ⇑ a : Ico 0 i, (⇑ b : Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry): WithBot ℤ)
= ⇑[H] a : Ico 0 i, ((⇑[(by sorry)] b: Ico a.1 i, (xs[b.1]'sorry)) - xs[a.1]'sorry) -- how to move (by sorry) to the list of parameters ?
:= by
calc ⇑ a : Ico 0 i, (⇑ b : Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry):WithBot ℤ)
_ = ⇑[H] a : Ico 0 i, (⇑ b: Ico a.1 i, ↑(xs[b.1]'sorry - xs[a.1]'sorry)) := by rw [← sup'_eq_sup];
_ = ⇑[H] a : Ico 0 i, (⇑[?_] b: Ico a.1 i, ↑(xs[b.1]'sorry - xs[a.1]'sorry)) := by congr! 1; rw [←sup'_eq_sup]; rw [univ_eq_attach, attach_nonempty_iff, nonempty_Ico]; sorry
_ = ⇑[H] a : Ico 0 i, (⇑[?_] b: Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry)) := by rw [coe_sup', ←sup'_eq_sup];
simp only [univ_eq_attach, Function.comp_apply]
simp; congr! 1; rw[←sup'_eq_sup]; congr
assumption;
simp_all only [univ_eq_attach]
simp_all only [attach_nonempty_iff, nonempty_Ico];
let x:= a.prop;
simp only [Nat.Ico_zero_eq_range, mem_range] at x
assumption
_ = ⇑[H] a : Ico 0 i, ((⇑[?_] b: Ico a.1 i, (xs[b.1]'sorry)) - xs[a.1]'sorry) := by congr! with a a';
conv =>
lhs
enter [3, b]
rw [Int.sub_eq_add_neg];
conv =>
lhs
rw [Finset.sup'_add_const _ (fun b => xs[b]'sorry) ]
. skip
. tactic => sorry
let x:=a.prop; simp at x ⊢; assumption
rfl
A. (Apr 23 2024 at 00:17):
I'd agree that your sup'_add_const looks overwrought given that this is possible:
theorem sup'_add_const {α : Type} {s : Finset α} (H : s.Nonempty) (f : α → ℤ) (c : ℤ) :
(sup' _ H (f · + c) ) = (sup' _ H f) + c :=
(comp_sup'_eq_sup'_comp H (· + c) (sup_add · · c)).symm
Vlad (Apr 23 2024 at 16:27):
Inspired by Alistair's answer, here's a bit shorter proof. Still quite long for such a trivial example
import Lean
import Mathlib.Tactic
open Lean Elab Term Meta
open Finset
open BigOperators
open Algebra
namespace BigOperators
open Std.ExtendedBinder PrettyPrinter Delaborator SubExpr
scoped syntax (name := bigmax) "⇑ " ("[" term "]" )? extBinder ", " term:67 : term
scoped macro_rules (kind := bigmax)
| `(⇑ $x:ident, $p) => `(Finset.sup Finset.univ (fun $x:ident ↦ $p))
| `(⇑ $x:ident : $t, $p) => `(Finset.sup Finset.univ (fun $x:ident : $t ↦ $p))
| `(⇑ [$hne] $x:ident : $t, $p ) => `(Finset.sup' Finset.univ $hne (fun $x:ident : $t ↦ $p))
scoped syntax (name := bigmaxin) "⇑ " extBinder " in " term ", " term:67 : term
scoped macro_rules (kind := bigmaxin)
| `(⇑ $x:ident in $s, $r) => `(Finset.sup $s (fun $x ↦ $r))
| `(⇑ $x:ident : $t in $s, $p) => `(Finset.sup $s (fun $x:ident : $t ↦ $p))
@[scoped delab app.Finset.sup] def delabFinsetSup : Delab := whenPPOption getPPNotation do
let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
guard <| f.isLambda
let ppDomain ← getPPOption getPPPiBinderTypes
let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
return (i, ← delab)
if s.isAppOfArity ``Finset.univ 2 then
let binder ←
if ppDomain then
let ty ← withNaryArg 1 delab
`(extBinder| $(.mk i):ident : $ty)
else
`(extBinder| $(.mk i):ident)
`(⇑ $binder, $body)
else
let ss ← withNaryArg 4 <| delab
`(⇑ $(.mk i):ident in $ss, $body)
end BigOperators
theorem Finset.sup'_add_const {α : Type} {s : Finset α} (H : s.Nonempty) (f : α → ℤ) (c : ℤ) :
(sup' _ H (f · + c) ) = (sup' _ H f) + c :=
(comp_sup'_eq_sup'_comp H (· + c) (sup_add · · c)).symm
theorem Finset.sup'_const_add {α : Type} {s: Finset α} (H : s.Nonempty) (f : α → ℤ) (c : ℤ) :
(sup' _ H (c + f ·) ) = c + (sup' _ H f) :=
by
rw [Int.add_comm, ←(sup'_add_const H _ c)]
simp [Int.add_comm]
example
(xs :Array ℤ)
(i: ℕ)
(hi1: i < xs.size)
(hi2: 0 < i)
{H: univ.Nonempty}
: ⇑ a : Ico 0 i, (⇑ b : Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry): WithBot ℤ)
= ((⇑[H] a : Ico 0 i, ((⇑[(by sorry)] b: Ico a.1 i, (xs[b.1]'sorry)) - xs[a.1]'sorry)):ℤ)
:= by
calc ⇑ a : Ico 0 i, (⇑ b : Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry):WithBot ℤ)
_ = ⇑[H] a : Ico 0 i, (⇑ b: Ico a.1 i, ↑(xs[b.1]'sorry - xs[a.1]'sorry)) := by rw [← sup'_eq_sup];
_ = ⇑[H] a : Ico 0 i, (⇑[?_] b: Ico a.1 i, ↑(xs[b.1]'sorry - xs[a.1]'sorry)) := by congr! 1; rw [←sup'_eq_sup]; rw [univ_eq_attach, attach_nonempty_iff, nonempty_Ico]; sorry
_ = ⇑[H] a : Ico 0 i, (⇑[?_] b: Ico a.1 i, (xs[b.1]'sorry - xs[a.1]'sorry)) := by rw [coe_sup', ←sup'_eq_sup];
simp only [univ_eq_attach, Function.comp_apply, coe_sup']
congr! 1; rw [←sup'_eq_sup]
congr!
trivial
sorry
_ = ⇑[H] a : Ico 0 i, ((⇑[?_] b: Ico a.1 i, (xs[b.1]'sorry)) - xs[a.1]'sorry) := by congr! with a a';
simp_rw [Int.sub_eq_add_neg]
rw [sup'_add_const _ _ (-xs[a.1]'sorry)]
let x:=a.prop; simp at x ⊢; assumption
rfl
Last updated: May 02 2025 at 03:31 UTC