Agda

[2025-10-25 Sat 01:43]

Interactive proving

See these examples from plfa.part1.Induction:

^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero rewrite *-zero-right n = refl
^-*-assoc m n (suc p)
  -- (m ^ n) ^ (suc p), simplified to m ^ n * (m ^ n) ^ p
  rewrite ^-*-assoc m n p
  -- m ^ n * m ^ (n * p)
        | sym (^-distrib-l-+-* m n (n * p))
  -- m ^ (n + n * p)
        | sym (*-suc n p)
  -- m ^ (n * suc p)
  = refl

-- try with ≡⟨⟩
^-*-assoc' : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc' m n zero rewrite *-zero-right n = refl
^-*-assoc' m n (suc p) =
  begin
    (m ^ n) ^ (suc p)
  ≡⟨⟩
    m ^ n * (m ^ n) ^ p
  ≡⟨ cong (_*_ (m ^ n)) (^-*-assoc m n p) ⟩
    m ^ n * m ^ (n * p)
  ≡⟨ sym (^-distrib-l-+-* m n (n * p)) ⟩
    m ^ (n + n * p)
  ≡⟨ cong (_^_ m) (sym (*-suc n p)) ⟩
    m ^ (n * suc p)
  ∎

With rewrite

My preferred syntax for interactivity is:

label : {type}
label {...}
label args
  rewrite {eq1}
        | {eq2}
        {...}
  = {!!}

That enables pretty nice interaction, including the ability to (un)comment lines quickly.

With ≡⟨⟩ (begin…qed)

When using ≡⟨⟩, put a hole in a justification slot. This will allow incremental progress both toward or away from the unification of the beginning and end terms.

begin
  from (inc b) + (from (inc b) + zero) -- (lhs)

-- keep adding (≡⟨⟩, equation) pairs here

≡⟨ {!!} ⟩

-- and/or here

  suc (from b + (from b + zero) + 1)   -- (rhs)
∎

Syntax

with as "extra arguments"

Consider this illumination from PLFA:

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                         =  forward z≤n
≤-total (suc m) zero                      =  flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n  =  forward (s≤s m≤n)
...                        | flipped n≤m  =  flipped (s≤s n≤m)

Every use of with is equivalent to defining a helper function. For example, the definition above is equivalent to the following:

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

What warranted a helper or with-abstraction? In the suc-suc case, we need to discriminate on the result of an intermediate computation. We might phrase our wish like this:

I wish that in this particular case, we could pass an extra argument that tells us how m and n are related.

Both where and with effectively do this, but the with syntax is most natural for that wish. It adds an expression, syntactically and conceptually, to the argument list. Because the extra argument is only present in the one case, pattern matching on that argument must immediately follow the case definition. So the form of with falls out of the wish for conditional extra arguments.

Further study

In some time, when I am ready, figure out what "simultaneous abstraction" is saying.