1.2. Right-associative And (Anne's solution)
Transform a sequence of Ands into a right-associative form (Anne's solution).
Example:
(a ∧ b) ∧ c => a ∧ b ∧ c
Contains versions that use:
-
assocand% - macrorules
-
assocandexpr% - Expr only
-
assocandqq% - Qq
namespace AndAssoc
namespace ElabExpr
open Lean Meta Elab
namespace Lean
-- Copied from Lean.Meta.AppBuilder
private def infer (h : Expr) : MetaM Expr := do
let hType ← inferType h
whnfD hType
-- Return (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)
def mkAndassoc (a b c : Expr) : Expr :=
mkApp3 (mkConst ``and_assoc) a b c
-- Return a ↔ a
def mkIffRefl (a : Expr) : MetaM Expr := do
let a ← whnf a
return mkApp (mkConst ``Iff.refl) a
def mkIffTrans (h₁ h₂ : Expr) : MetaM Expr := do
let t₁ ← infer h₁
let t₂ ← infer h₂
match t₁.iff?, t₂.iff? with
| some (a, b), some (_, c) =>
return mkApp5 (mkConst ``Iff.trans) a b c h₁ h₂
| none, _ => throwError m!"mkIffTrans: {h₁} is not an Iff"
| _, none => throwError m!"mkIffTrans: {h₂} is not an Iff"
def mkAndCongr (h₁ h₂ : Expr) : MetaM Expr := do
let t₁ ← infer h₁
let t₂ ← infer h₂
match t₁.iff?, t₂.iff? with
| some (a, c), some (b, d) =>
return mkAppN (mkConst ``and_congr) #[a, c, b, d, h₁, h₂]
| none, _ => throwError m!"mkAndCongr: {h₁} is not an Iff"
| _, none => throwError m!"mkAndCongr: {h₂} is not an Iff"
end Lean
/-- Given `a` a right associated And, and any `b`, return `(Q, a ∧ b ↔ Q)` where`Q`
is `a` with `b` added to the right-most conjunction.
Example:
merge (x ∧ (y ∧ z)) (x' ∧ y') => (x ∧ (y ∧ (z ∧ (x' ∧ y'))), pf)
-/
partial def merge (a b : Expr) : MetaM (Expr × Expr) := do
match_expr a with
| And a1 a2 =>
-- a2 ∧ b ↔ right_assoc a2 ∧ b
let (a2_b, a2_b_iff) ← merge a2 b
-- Q := a1 ∧ (right2_assoc a2 ∧ b)
let Q := Lean.mkAnd a1 a2_b
-- (a1 ∧ a2) ∧ b ↔ a1 ∧ (a2 ∧ b)
let a1_a2_b_iff := Lean.mkAndassoc a1 a2 b
-- a1 ↔ a1
let a1Refl ← Lean.mkIffRefl a1
-- a1 ∧ (a2 ∧ b) ↔ a1 ∧ (right_assoc a2 ∧ b)
let a1_a2_b_assoc_iff ← Lean.mkAndCongr a1Refl a2_b_iff
-- (a1 ∧ a2) ∧ b ↔ a1 ∧ (right_assoc a2 ∧ b)
let iff ← Lean.mkIffTrans a1_a2_b_iff a1_a2_b_assoc_iff
return (Q, iff)
| _ => do
let Q := Lean.mkAnd a b
let iff ← Lean.mkIffRefl Q
return (Q, iff)
/-- Transform a sequence of `And`s into a right-associative form, and return a proof
that the input and output terms are equivalent.
Example:
assocAndProof ((a ∧ b) ∧ c) => (a ∧ b ∧ c, pf) : Prop ×' ((a ∧ b) ∧ c) ↔ a ∧ b ∧ c
-/
partial def assocAndProof (a : Expr) : MetaM (Expr × Expr) := do
match_expr a with
| And a1 a2 =>
-- a1 ↔ right_assoc a1
let (a1_assoc, a1_assoc_iff) ← assocAndProof a1
-- a2 ↔ right_assoc a2
let (a2_assoc, a2_assoc_iff) ← assocAndProof a2
-- a1 ∧ a2 ↔ right_assoc a1 ∧ right_assoc a2
let a1_a2_assoc_iff ← Lean.mkAndCongr a1_assoc_iff a2_assoc_iff
-- right_assoc a1 ∧ right_assoc a2 ↔ right_assoc a1 ∧ a2
let (Q, mergeIff) ← merge a1_assoc a2_assoc
-- a1 ∧ a2 ↔ right_assoc a1 ∧ a2
let pf ← Lean.mkIffTrans a1_a2_assoc_iff mergeIff
return (Q, pf)
| _ => do
let aRefl ← mkAppM ``Iff.refl #[a]
return (a, aRefl)
elab "assoc_and_proof* " t:term : term => do
let expr ← Term.elabTerm t none
let (Q, p) ← assocAndProof expr
mkAppM ``PProd.mk #[Q, p]
namespace Test
variable (a b c d e : Prop)
def test1 := assoc_and_proof* a
example : (test1 a).fst = a := rfl
example : a ↔ a := (test1 a).snd
def test2 := assoc_and_proof* (a ∧ b) ∧ c
example : (test2 a b c).fst = (a ∧ b ∧ c) := rfl
example : ((a ∧ b) ∧ c) ↔ a ∧ b ∧ c := (test2 a b c).snd
def test3 := assoc_and_proof* a ∧ (b ∧ c)
example : (test3 a b c).fst = (a ∧ b ∧ c) := rfl
example : a ∧ (b ∧ c) ↔ a ∧ b ∧ c := (test3 a b c).snd
def test4 := assoc_and_proof* ((a ∧ b) ∧ c) ∧ (d ∧ e)
example : (test4 a b c d e).fst = (a ∧ b ∧ c ∧ d ∧ e) := rfl
example : ((a ∧ b) ∧ c) ∧ (d ∧ e) ↔ a ∧ b ∧ c ∧ d ∧ e := (test4 a b c d e).snd
end Test
end ElabExpr
namespace ElabQq
open Lean Meta Elab Qq
/-- Given `a` a right associated And, and any `b`, return `(Q, a ∧ b ↔ Q)` where`Q`
is `a` with `b` added to the right-most conjunction.
Example:
merge (x ∧ (y ∧ z)) (x' ∧ y') => (x ∧ (y ∧ (z ∧ (x' ∧ y'))), pf)
-/
partial def merge (a b : Q(Prop)) : MetaM ((Q : Q(Prop)) × Q($a ∧ $b ↔ $Q)) := do
match a with
| ~q($a1 ∧ $a2) =>
-- a2 ∧ b ↔ right_assoc a2 ∧ b
let ⟨a2_b, a2_b_iff⟩ ← merge a2 b
-- (a1 ∧ a2) ∧ b ↔ a1 ∧ (right_assoc a2 ∧ b)
return ⟨q($a1 ∧ $a2_b), q(Iff.trans and_assoc (and_congr Iff.rfl $a2_b_iff))⟩
| _ =>
return ⟨q($a ∧ $b), q(Iff.rfl)⟩
/-- Transform a sequence of `And`s into a right-associative form, and return a proof
that the input and output terms are equivalent.
Example:
assocAndProof ((a ∧ b) ∧ c) => (a ∧ b ∧ c, pf) : Prop ×' ((a ∧ b) ∧ c) ↔ a ∧ b ∧ c
-/
partial def assocAndProof (a : Q(Prop)) : MetaM ((Q : Q(Prop)) × Q($a ↔ $Q)) := do
match a with
| ~q($a1 ∧ $a2) =>
-- a1 ↔ right_assoc a1
let ⟨a1_assoc, a1_iff⟩ ← assocAndProof a1
-- a2 ↔ right_assoc a2
let ⟨a2_assoc, a2_iff⟩ ← assocAndProof a2
-- right_assoc a1 ∧ right_assoc a2 ↔ right_assoc a1 ∧ a2
let ⟨Q, mergeIff⟩ ← merge a1_assoc a2_assoc
-- a1 ∧ a2 ↔ right_assoc a1 ∧ a2
return ⟨Q, q(Iff.trans (and_congr $a1_iff $a2_iff) $mergeIff)⟩
| _ =>
return ⟨a, q(Iff.rfl)⟩
elab "assoc_and_proof_qq* " t:term : term => do
let P ← Term.elabTerm t none
let ⟨1, ~q(Prop), P⟩ ← inferTypeQ P | throwError m!"{P} is not a Prop"
let ⟨Q, p⟩ ← assocAndProof P
return q((⟨$Q, $p⟩ : Prop ×' ($P ↔ $Q)))
namespace Test
variable (a b c d e : Prop)
def test1 := assoc_and_proof_qq* a
example : (test1 a).fst = a := rfl
example : a ↔ a := (test1 a).snd
def test2 := assoc_and_proof_qq* (a ∧ b) ∧ c
example : (test2 a b c).fst = (a ∧ b ∧ c) := rfl
example : ((a ∧ b) ∧ c) ↔ a ∧ b ∧ c := (test2 a b c).snd
def test3 := assoc_and_proof_qq* a ∧ (b ∧ c)
example : (test3 a b c).fst = (a ∧ b ∧ c) := rfl
example : a ∧ (b ∧ c) ↔ a ∧ b ∧ c := (test3 a b c).snd
def test4 := assoc_and_proof_qq* ((a ∧ b) ∧ c) ∧ (d ∧ e)
example : (test4 a b c d e).fst = (a ∧ b ∧ c ∧ d ∧ e) := rfl
example : ((a ∧ b) ∧ c) ∧ (d ∧ e) ↔ a ∧ b ∧ c ∧ d ∧ e := (test4 a b c d e).snd
/-- error: 1 is not a Prop -/
#guard_msgs in
#check assoc_and_proof_qq* 1
end Test
end ElabQq
-- A linear version of the elaborator by Anne Baanen
namespace ElabQqLinear
open Lean Meta Elab Qq
/--
Conjunction but the right hand side might be empty.
`and? a (some b)` is `a ∧ b`, `and? a none` is `a`.
-/
def and? (a : Q(Prop)) : Option Q(Prop) → Q(Prop)
| none => a
| some b => q($a ∧ $b)
/-- Assembles proofs for subproblems into one large proof. -/
def prove (a1 a2 a2_assoc Q : Q(Prop)) (acc : Option Q(Prop))
(a2_iff : Q($(and? a2 acc) ↔ $a2_assoc))
(merge_iff : Q($a1 ∧ $a2_assoc ↔ $Q)) : MetaM Q($(and? q($a1 ∧ $a2) acc) ↔ $Q) := do
match acc with
| some _ =>
-- I might also consider extracting the term below as a `lemma`,
-- since it is not totally trivial to read what's going on here.
return q((and_assoc.trans (and_congr_right' $a2_iff)).trans $merge_iff)
| none => return q(Iff.trans (and_congr_right' $a2_iff) $merge_iff)
/-- Accumulating version of `assocAndProof`. Reassociate `And`s in
`a ∧ acc` to the right, where `acc` is already right-associated.
`acc` can potentially be `none` (in which case we reassociate `a` only).
-/
partial def assocAcc (a : Q(Prop)) (acc : Option Q(Prop) := none) :
MetaM ((Q : Q(Prop)) × Q($(and? a acc) ↔ $Q)) := do
match a with
| ~q($a1 ∧ $a2) =>
let ⟨a2_assoc, a2_iff⟩ ← assocAcc a2 acc
let ⟨Q, merge_iff⟩ ← assocAcc a1 a2_assoc
-- Ideally I'd inline `prove` here but Qq complains about the pattern match...
return ⟨Q, ← prove a1 a2 a2_assoc Q acc a2_iff merge_iff⟩
| _ => match acc with
| some b =>
return ⟨q($a ∧ $b), q(Iff.rfl)⟩
| none =>
return ⟨a, q(Iff.rfl)⟩
elab "assoc_and_proof_qq2* " t:term : term => do
let P ← Term.elabTerm t none
let ⟨1, ~q(Prop), P⟩ ← inferTypeQ P | throwError m!"{P} is not a Prop"
let ⟨Q, p⟩ ← assocAcc P
return q((⟨$Q, $p⟩ : Prop ×' ($P ↔ $Q)))
namespace Test
variable (a b c d e : Prop)
def test1_2 := assoc_and_proof_qq2* a
example : (test1_2 a).fst = a := rfl
example : a ↔ a := (test1_2 a).snd
def test2_2 := assoc_and_proof_qq* (a ∧ b) ∧ c
example : (test2_2 a b c).fst = (a ∧ b ∧ c) := rfl
example : ((a ∧ b) ∧ c) ↔ a ∧ b ∧ c := (test2_2 a b c).snd
def test3_2 := assoc_and_proof_qq* a ∧ (b ∧ c)
example : (test3_2 a b c).fst = (a ∧ b ∧ c) := rfl
example : a ∧ (b ∧ c) ↔ a ∧ b ∧ c := (test3_2 a b c).snd
def test4_2 := assoc_and_proof_qq* ((a ∧ b) ∧ c) ∧ (d ∧ e)
example : (test4_2 a b c d e).fst = (a ∧ b ∧ c ∧ d ∧ e) := rfl
example : ((a ∧ b) ∧ c) ∧ (d ∧ e) ↔ a ∧ b ∧ c ∧ d ∧ e := (test4_2 a b c d e).snd
end Test
end ElabQqLinear
end AndAssoc