Lean

Posts

• HEq and Axiom K: An Exploration in Lean
  February 23, 2026

  berberman

  • Lean

  While reading Conor McBride's A Few Constructions on Constructors, I came across his definition of Heterogeneous Equality (represented here using Lean axioms):

  Read more
• Dependent Pattern Matching and Convoy Patterns
  April 18, 2026

  berberman

  • Lean

  The other day, I saw my friend CircuitCoder ask a Rocq question in a group chat:

  "How do you prove the following theorem without using the dependent destruction tactic? It seems to require the Convoy Pattern, which I tried learning but still don't quite grasp."

  Inductive vector (A : Type) : nat -> Type :=
    | vnil : vector A 0
    | vcons {n} (v : vector A n) (a : A) : vector A (S n).
  
  Lemma test {A} {n} {v : vector A (S n)} :
    exists v' : vector A n, exists a : A, v = vcons A v' a.
  

  Let's explore dependent pattern matching and the convoy pattern in Lean!

  Read more