Skip to content

feat: Vec delab #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Equilibris merged 4 commits into from
Aug 21, 2025
Merged

feat: Vec delab #61

Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
45caf77
feat: Vec delab
Aug 20, 2025
304e14c
refactor: remove unneeded abstraction
Aug 20, 2025
79b2563
fix: remove [_;_] notation
Aug 21, 2025
86e3acd
refactor: remove line break
Equilibris Aug 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 25 additions & 7 deletions Qpf/Util/Vec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,28 +67,46 @@ end Vec
-/

syntax "!![" term,* "]" : term
syntax "!![" term ";" term,* "]" : term
macro_rules
| `(!![]) => `(Vec.nil)
| `(!![$x]) => `(Vec.append1 !![] $x)
| `(!![ $xs,* , $x]) => `(Vec.append1 !![$xs,*] $x)

| `(!![$t; ]) => `($t)
| `(!![$t; $x]) => `(Vec.append1 $t $x)
| `(!![$t; $xs,* , $x]) => `(Vec.append1 !![$t; $xs,*] $x)
Copy link
Owner

@alexkeizer alexkeizer Aug 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do you mix semi-colons and commas here? Did you mean to change the syntax?



namespace Vec
@[app_unexpander Vec.nil]
def nil_uex : Lean.PrettyPrinter.Unexpander
| `($_p) => `(!![])

@[app_unexpander Vec.append1]
def append1_uex : Lean.PrettyPrinter.Unexpander
| `($_p !![$x,*] $r) => `(!![$(x.push r),* ])
| `($_p !![$t; $x,*] $r) => `(!![$t; $(x.push r),* ])
| _ => throw () -- unhandled

/-- info: !![ℤ, ℕ, Prop] : Vec Type (Nat.succ 0).succ.succ -/
#guard_msgs in
#check !![ℤ, ℕ, Prop]
Copy link
Owner

@alexkeizer alexkeizer Aug 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! Adding an unexpander for this syntax is a really good idea!

Note that standard Lean/Mathlib style does not indent after a section or namespace.
QPFTypes largely does not follow this style, but we probably should for new code so that eventually we are consistent.

That is, please remove the indentation here; but don't worry about the rest of the file (unless you feel particularly inspired to make a separate style cleanup PR)



theorem drop_append1 {v : Vec α n} {a : α} {i : PFin2 n} :
drop (append1 v a) i = v i :=
drop !![v; a] i = v i :=
rfl

theorem drop_append1' {v : Vec α n} {a : α} :
drop (append1 v a) = v :=
drop !![v; a] = v :=
by funext x; rfl

theorem last_append1 {v : Vec α n} {a : α} :
last (append1 v a) = a
last !![v; a] = a
:= rfl

@[simp]
theorem append1_drop_last (v : Vec α (n+1)) : append1 (drop v) (last v) = v :=
theorem append1_drop_last (v : Vec α (n+1)) : !![drop v; last v] = v :=
funext $ fun i => by cases i; rfl; rfl


Expand Down Expand Up @@ -197,8 +215,8 @@ namespace Vec
induction as;
case nil => rfl
case cons a as ih =>
simp only [toList, ofList, append1, last, DVec.last, drop_append1', ih]
rfl
change a :: (ofList as).toList = a :: _
rw [ih]

instance : Coe (Vec (Type u) n) (TypeVec.{u} n) where
coe v i := v i
Expand Down