Multi-prover documents

Alectryon documents can use multiple provers. Inputs for each prover are processed independently.

To compile:

alectryon polyglot.rst
    # reST+… → HTML;  produces ‘polyglot.html’

Require Import PeanoNat.

Lemma mul_comm :
  forall a b: nat, a * b = b * a.
forall a b : nat, a * b = b * a
Proof.
forall a b : nat, a * b = b * a
  induction a; simpl.
forall b : nat, 0 = b * 0
a: nat
IHa: forall b : nat, a * b = b * a
forall b : nat, b + a * b = b * S a
  -
forall b : nat, 0 = b * 0 induction b; simpl; congruence.
  -
a: nat
IHa: forall b : nat, a * b = b * a
forall b : nat, b + a * b = b * S a induction b; simpl.
a: nat
IHa: forall b : nat, a * b = b * a
a * 0 = 0
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + a * S b) = S (a + b * S a)
    +
a: nat
IHa: forall b : nat, a * b = b * a
a * 0 = 0 rewrite IHa; reflexivity.
    +
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + a * S b) = S (a + b * S a) rewrite <- IHb, IHa.
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + S b * a) = S (a + (b + a * b))
      simpl.
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + (a + b * a)) = S (a + (b + a * b)) rewrite IHa.
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + (a + b * a)) = S (a + (b + b * a))
      rewrite !Nat.add_assoc.
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (b + a + b * a) = S (a + b + b * a)
      rewrite (Nat.add_comm b a).
a: nat
IHa: forall b : nat, a * b = b * a
b: nat
IHb: b + a * b = b * S a
S (a + b + b * a) = S (a + b + b * a)
      reflexivity.
Qed.

open Nat

def customSum : Nat -> Nat
  | 0      => 0
  | succ n => succ n + customSum n

#eval
55
 customSum 10

namespace Nat
  theorem mul_two : ∀ n : Nat, 2 * n = n + n := by
∀ (n : Nat), 2 * n = n + n
    intros n
n: Nat
2 * n = n + n
    induction n with
n: Nat
2 * n = n + n
    | zero =>
zero
2 * zero = zero + zero simp
Goals accomplished! 🐙
    | succ n n_ih =>
n: Nat
n_ih: 2 * n = n + n
succ
2 * succ n = succ n + succ n
      rw [
n: Nat
n_ih: 2 * n = n + n
succ
2 * succ n = succ n + succ n← Nat.add_one,
n: Nat
n_ih: 2 * n = n + n
succ
2 * (n + 1) = n + 1 + (n + 1) Nat.left_distrib,
n: Nat
n_ih: 2 * n = n + n
succ
2 * n + 2 * 1 = n + 1 + (n + 1) n_ih
n: Nat
n_ih: 2 * n = n + n
succ
n + n + 2 * 1 = n + 1 + (n + 1)]
n: Nat
n_ih: 2 * n = n + n
succ
n + n + 2 * 1 = n + 1 + (n + 1)
      simp [Nat.add_assoc, Nat.add_comm 1]
Goals accomplished! 🐙

  theorem gauss : ∀ n : Nat, 2 * customSum n = n * (n + 1) := by
∀ (n : Nat), 2 * customSum n = n * (n + 1)
    intros n
n: Nat
2 * customSum n = n * (n + 1)
    induction n with
n: Nat
2 * customSum n = n * (n + 1)
    | zero =>
zero
2 * customSum zero = zero * (zero + 1) simp [customSum]
Goals accomplished! 🐙
    | succ n n_ih =>
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * customSum (succ n) = succ n * (succ n + 1)
      simp [customSum]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * (succ n + customSum n) = succ n * (succ n + 1)
      simp [Nat.left_distrib]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * succ n + 2 * customSum n = succ n * succ n + succ n
      rw [
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * succ n + 2 * customSum n = succ n * succ n + succ nn_ih,
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * succ n + n * (n + 1) = succ n * succ n + succ n ← Nat.add_one
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * (n + 1) + n * (n + 1) = (n + 1) * (n + 1) + (n + 1)]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
2 * (n + 1) + n * (n + 1) = (n + 1) * (n + 1) + (n + 1)
      simp [Nat.left_distrib, Nat.right_distrib,
            Nat.mul_one, Nat.one_mul, Nat.mul_two]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n + n + 2 + (n * n + n) = n * n + n + (n + 1) + (n + 1)
      rw [
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n + n + 2 + (n * n + n) = n * n + n + (n + 1) + (n + 1)Nat.add_comm
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + n + (n + n + 2) = n * n + n + (n + 1) + (n + 1)]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + n + (n + n + 2) = n * n + n + (n + 1) + (n + 1)
      simp [Nat.add_assoc]
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + (n + (n + (n + 2))) = n * n + (n + (n + (1 + (n + 1))))
      rw [
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + (n + (n + (n + 2))) = n * n + (n + (n + (1 + (n + 1))))Nat.add_one,
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + (n + (n + succ (n + 1))) = n * n + (n + (n + (1 + (n + 1)))) Nat.add_comm 1
n: Nat
n_ih: 2 * customSum n = n * (n + 1)
succ
n * n + (n + (n + succ (n + 1))) = n * n + (n + (n + (n + 1 + 1)))]
Goals accomplished! 🐙
end Nat