1.1. Right-associative And
Transform a sequence of Ands into a right-associative form.
Example:
(a ∧ b) ∧ c => a ∧ b ∧ c
Contains versions that use:
-
assoc_and%-macro_rules -
assoc_and_expr%- Expr only -
assoc_and_qq%- Qq
namespace AndAssoc
namespace Macro
/-- A macro version of the expression transform -/
syntax (name := assocAnd) "assoc_and% " term : term
macro_rules
| `(assoc_and% ($a ∧ $b) ∧ $c) => `(assoc_and% $a ∧ $b ∧ $c)
| `(assoc_and% $a ∧ $b) => `($a ∧ assoc_and% $b)
| `(assoc_and% ($e)) => `(assoc_and% $e)
| `(assoc_and% $e) => `($e)
section Test
variable
(a b c d e: Prop)
/-- info: a : Prop -/
#guard_msgs in
#check assoc_and% a
/-- info: a : Prop -/
#guard_msgs in
#check assoc_and% (a)
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and% ((a ∧ b) ∧ c)
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and% (a ∧ b) ∧ c
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and% a ∧ (b ∧ c)
/-- info: a ∧ b ∧ c ∧ d ∧ e : Prop -/
#guard_msgs in
#check assoc_and% ((a ∧ b) ∧ c) ∧ (d ∧ e)
end Test
end Macro
universe u
-- Similar to Haskell NonEmpty. Does this exist in Lean stdlib?
structure NonEmptyList (α : Type u) where
head : α
tail : List α
instance {α : Type u} : Append (NonEmptyList α) where
append l1 l2 := ⟨l1.head, l1.tail ++ l2.head :: l2.tail⟩
namespace Expr
open Lean Meta Elab Qq
def collectArgs : Expr → NonEmptyList Expr
| .app (.app (.const ``And _) a) b => collectArgs a ++ collectArgs b
| e => ⟨e, []⟩
def rightAssoc (head : Expr) : List Expr → Expr
| [] => head
| x :: xs => mkApp2 (mkConst ``And) head (rightAssoc x xs)
def assocAndMeta (e : Expr) : Expr :=
let args := collectArgs e
rightAssoc args.head args.tail
/-- An elab version of the expression transform -/
elab "assoc_and_expr% " t:term : term => do
let expr ← Term.elabTerm t none
assocAndMeta expr |> pure
section Test
variable
(a b c d e: Prop)
/-- info: a : Prop -/
#guard_msgs in
#check assoc_and_expr% a
/-- info: a : Prop -/
#guard_msgs in
#check assoc_and_expr% (a)
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and_expr% ((a ∧ b) ∧ c)
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and_expr% (a ∧ b) ∧ c
/-- info: a ∧ b ∧ c : Prop -/
#guard_msgs in
#check assoc_and_expr% a ∧ (b ∧ c)
/-- info: a ∧ b ∧ c ∧ d ∧ e : Prop -/
#guard_msgs in
#check assoc_and_expr% ((a ∧ b) ∧ c) ∧ (d ∧ e)
end Test
end Expr
namespace MetaMQq
open Lean Meta Elab Qq
def rightAssocQ (head: Q(Prop)) : List Q(Prop) → MetaM Q(Prop)
| [] => head |> pure
| x :: xs => do
let tail ← rightAssocQ x xs
q($head ∧ $tail) |> pure
partial def collectArgsQ : Q(Prop) → MetaM (NonEmptyList Q(Prop))
| ~q($a ∧ $b) => return (← collectArgsQ a) ++ (← collectArgsQ b)
| ~q($e) => return ⟨e, []⟩
def assocAndMetaQ (e : Expr) : MetaM Expr := do
let ⟨1, ~q(Prop), e⟩ ← inferTypeQ e | throwError m!"{e} is not a Prop"
let args ← collectArgsQ e
rightAssocQ args.head args.tail
/-- A Qq version of the expression transform -/
elab "assoc_and_qq% " t:term : term => do
let expr ← Term.elabTerm t none
assocAndMetaQ expr
1.1.1. Tests
section Test
variable
(a b c d e: Prop)
#check assoc_and_qq% a
#check assoc_and_qq% (a)
#check assoc_and_qq% ((a ∧ b) ∧ c)
#check assoc_and_qq% (a ∧ b) ∧ c
#check assoc_and_qq% a ∧ (b ∧ c)
#check assoc_and_qq% ((a ∧ b) ∧ c) ∧ (d ∧ e)
#check assoc_and_qq% 1
end Test
end MetaMQq
end AndAssoc