tactic by (boolean?) reflection example

Stream: mathlib4

[Joachim Breitner]

What is a good tactic whose code I could cargo cult from for a reflection-style normalizer or solver tactic?
I hope I am using the term correctly; I mean the approach where

• I define a “normal” data type to describe the problem
• a tactic that parses the goal state into this data type
• a function that converts it back so that the tactic can replace the goal with that function applied to my custom data type
• a function that solves or normalizes the value, with a proof that it’s correct
• and then using that proof to conclude the tactic
  (Maybe this is called “boolean reflection”?)

[Joachim Breitner]

Some more googling may indicate that this style of boolean reflection isn’t actually a common technique in lean? Or is that just not the right term around here? I have also seen the name “small-scale reflection”.

[James Gallicchio]

maybe linarith? it's the only tactic I know that currently does something along those lines...

[Eric Wieser]

matrix.mulᵣ_eq was my attempt at this in Lean3, though the meta portion never got merged

[Wojciech Nawrocki]

@Joachim Breitner yeah, proof by reflection is almost not used at all in mathlib. This, afaik, is because historically the kernel didn't support it very well, i.e. reflection was slow. In mathlib3, the ring2 tactic proceeds by reflection. But it is more common to do the normalisation at the meta-level, and construct a proof of its correctness (e.g. using Eq.rec) as we go.

[Mario Carneiro]

Here's a simple tautology tactic using proof by reflection:

import Mathlib.Util.AtomM

inductive Formula : Type
  | var : Nat → Formula
  | not : Formula → Formula
  | imp : Formula → Formula → Formula
  deriving Inhabited

namespace Formula
def eval (V : List Bool) : Formula → Bool
  | .var n => V.getD n false
  | .not f => ¬ f.eval V
  | .imp f₁ f₂ => f₁.eval V → f₂.eval V

def eval' (F : List Prop) : Formula → Prop
  | .var n => F.getD n False
  | .not f => ¬ f.eval' F
  | .imp f₁ f₂ => f₁.eval' F → f₂.eval' F

def taut : Nat → List Bool → Formula → Bool
  | 0, V, f => f.eval V
  | n+1, V, f => f.taut n (false::V) && f.taut n (true::V)

theorem eval_map (V : List Bool) (f : Formula) : f.eval' (V.map (· = true)) ↔ f.eval V := by
  induction f <;> simp [eval', eval, *, List.getD]
  rename_i n
  induction V generalizing n <;> simp [List.get?]
  · simp [Option.getD]
  · match n with
    | 0 => simp [List.get?, Option.getD]
    | n+1 => simp [List.get?, *]

theorem exists_val : ∀ F : List Prop, ∃ V : List Bool, F = V.map (· = true)
  | [] => ⟨[], rfl⟩
  | p::F => by
    let ⟨V, e⟩ := exists_val F
    by_cases h : p
    · exact ⟨true::V, by simp [e, List.map, h]⟩
    · exact ⟨false::V, by simp [e, List.map, h]⟩

theorem eval_of_taut :
    ∀ (V W : List Bool) (f : Formula), f.taut V.length W → f.eval (V.reverseAux W)
  | [], W, f => by simp [taut]
  | v::V, W, f => by
    simp [taut]
    intro h₁ h₂
    have := eval_of_taut V (v::W) f
    cases v
    · exact this h₁
    · exact this h₂

theorem eval'_of_taut (F : List Prop) (f : Formula) (h : f.taut F.length []) : f.eval' F := by
  let ⟨V, e⟩ := exists_val F
  subst e
  rw [List.length_map] at h
  rw [eval_map]
  have : _ → f.eval V.reverse.reverse := eval_of_taut V.reverse [] f
  rw [List.length_reverse, List.reverse_reverse] at this
  exact this h

end Formula

open Mathlib.Tactic Qq

abbrev imp (p q : Prop) : Prop := p → q -- workaround for QQ bug?
partial def parseExpr (e : Q(Prop)) : AtomM Q(Formula) := do
  match e with
  | ~q(¬$p) => return q(.not $(← parseExpr p))
  | ~q(imp $p $q) => return q(.imp $(← parseExpr p) $(← parseExpr q))
  | ~q($e) => have n : Q(ℕ) := Lean.mkNatLit (← AtomM.addAtom e); return q(.var $n)

open Lean Elab Tactic
elab "taut" : tactic => liftMetaTactic fun g => do
  let some (ty : Q(Prop)) ← checkTypeQ (← g.getType) (q(Prop) : Q(Type)) | failure
  let (f, atoms) ← AtomM.run .default do pure (← parseExpr ty, (← get).atoms)
  have F : Q(List Prop) := atoms.foldr (fun (a : Q(Prop)) ls => q($a :: $ls)) q([])
  let pf : Q(($f).taut ($F).length [] = true) := (q(Eq.refl true) : Expr)
  g.assign q(Formula.eval'_of_taut $F $f $pf)
  pure []

example (p q : Prop) : p → q → p := by taut
example : (¬1 = 2 → 1 = 2) → 1 = 2 := by taut
example : ¬p → ¬p := by taut

[Mario Carneiro]

I have also seen the name “small-scale reflection”.

This is not small-scale reflection. Boolean reflection in this style is "large-scale reflection", while ssreflect deals with using reflection to perform rewrites and other small reductions in the course of a proof. Large-scale reflection is characterized by having a single kernel proof goal like myFunc = true which does almost all of the actual proof work.

[Mario Carneiro]

@Joachim Breitner

[Joachim Breitner]

Cool, thanks for that example! Not too much boiler-plate code it seems.