2.1. Reducing functions defined via well-founded recursion🔗

The countdown function below uses well-founded recursion, forced by the explicit termination_by.

def countdown (n : Nat) : List Nat :=
  match n with
  | 0 => [0]
  | n' + 1 => (n' + 1) :: countdown n'
  termination_by n

Because it is defined by well-founded recursion, countdown 3 is not definitionally equal to its value, so rfl fails:

theorem countdown_rfl : countdown 3 = [3, 2, 1, 0] := by⊢ countdown 3 = [3, 2, 1, 0] Tactic `rfl` failed: The left-hand side
  countdown 3
is not definitionally equal to the right-hand side
  [3, 2, 1, 0]

⊢ countdown 3 = [3, 2, 1, 0]rfl⊢ countdown 3 = [3, 2, 1, 0]

Tactic `rfl` failed: The left-hand side
  countdown 3
is not definitionally equal to the right-hand side
  [3, 2, 1, 0]

⊢ countdown 3 = [3, 2, 1, 0]

The cbv tactic reduces it anyway, using the function's equation lemmas:

theorem countdown_cbv : countdown 3 = [3, 2, 1, 0] := by⊢ countdown 3 = [3, 2, 1, 0] cbvAll goals completed! 🐙

cbv produces a proof term. Printing countdown_cbv shows the equation lemmas (countdown.eq_1, countdown.eq_2) being chained together.

theorem Probe.countdown_cbv : countdown 3 = [3, 2, 1, 0] :=
of_eq_true
  (Eq.trans
    (congrFun'
      (congrArg Eq
        (Eq.trans (countdown.eq_2 2)
          (congr (congrArg List.cons (Eq.refl 3))
            (Eq.trans (countdown.eq_2 1)
              (congr (congrArg List.cons (Eq.refl 2))
                (Eq.trans (countdown.eq_2 0) (congr (congrArg List.cons (Eq.refl 1)) countdown.eq_1)))))))
      [3, 2, 1, 0])
    (eq_self [3, 2, 1, 0]))#print countdown_cbv

theorem Probe.countdown_cbv : countdown 3 = [3, 2, 1, 0] :=
of_eq_true
  (Eq.trans
    (congrFun'
      (congrArg Eq
        (Eq.trans (countdown.eq_2 2)
          (congr (congrArg List.cons (Eq.refl 3))
            (Eq.trans (countdown.eq_2 1)
              (congr (congrArg List.cons (Eq.refl 2))
                (Eq.trans (countdown.eq_2 0) (congr (congrArg List.cons (Eq.refl 1)) countdown.eq_1)))))))
      [3, 2, 1, 0])
    (eq_self [3, 2, 1, 0]))