Generating minified HTML

Alectryon normally produces plain HTML files. For very large proofs, these files can get quite large (sometimes hundreds of megabytes), but they also tend to be highly redundant; hence, Alectryon also has the ability to generate “minified” HTML files, which contain special pointers (“backreferences”) to previous parts of the document. These backreferences are resolved dynamically when the page is displayed in a web browser.

Here is an example proof, written in a way that generates lots of redundant objects (for example, section variables appear in the proof context at every step of the proof):

Require Import List.
Import ListNotations.

Section Folds.
  Context {A} (op: A -> A -> A) (init: A).
  Context (init_comm: forall a, op init a = op a init).
  Context (op_assoc: forall x y z, op (op x y) z = op x (op y z)).

Step 1: prove that init can be moved around:

  
fold_right = 
fun (A B : Type) (f : B -> A -> A) (a0 : A) =>
fix fold_right (l : list B) : A :=
  match l with
  | [] => a0
  | b :: t => f b (fold_right t)
  end
     : forall A B : Type,
       (B -> A -> A) -> A -> list B -> A

Arguments fold_right [A B]%type_scope _%function_scope
  _ _%list_scope
  Lemma init_comm' l:
    forall a, fold_left op l (op init a) = op a (fold_left op l init).
A:Type
op:A -> A -> A
init:A
init_comm:forall a : A, op init a = op a init
op_assoc:forall x y z : A,
op (op x y) z = op x (op y z)
l:list A
forall a : A,
fold_left op l (op init a) =
op a (fold_left op l init)
  Proof.
2
    induction l.
56789
forall a : A,
fold_left op [] (op init a) =
op a (fold_left op [] init)
56789
a:A
a
IHl:forall a : A,
fold_left op l (op init a) =
op a (fold_left op l init)
forall a0 : A,
fold_left op (a :: l) (op init a0) =
op a0 (fold_left op (a :: l) init) all: simpl.
10
forall a : A, op init a = op a init
14
forall a0 : A,
fold_left op l (op (op init a0) a) =
op a0 (fold_left op l (op init a)) all: intros.
5678915
op init a = op a init
5678915a16
a0:A
fold_left op l (op (op init a0) a) =
op a0 (fold_left op l (op init a))
    -
21 eauto using init_comm.
    -
26
28 rewrite op_assoc.
26
fold_left op l (op init (op a0 a)) =
op a0 (fold_left op l (op init a))
      rewrite IHl.
26
op (op a0 a) (fold_left op l init) =
op a0 (fold_left op l (op init a))
      rewrite op_assoc.
26
op a0 (op a (fold_left op l init)) =
op a0 (fold_left op l (op init a))
      rewrite <- IHl.
26
op a0 (fold_left op l (op init a)) =
op a0 (fold_left op l (op init a))
      reflexivity.
  Qed.

Step 2: prove that fold_left and fold_right are equivalent.

  Goal forall l, fold_left op l init = fold_right op init l.
10
forall l : list A,
fold_left op l init = fold_right op init l
  Proof.
3f
    intros.
4
fold_left op l init = fold_right op init l pose (l' := l).
56789a
l':=l:list A
46
    induction l.
56789
l':=[]:list A
fold_left op [] init = fold_right op init []
5678915a
l':=a :: l:list A
IHl:let l' := l in
fold_left op l init = fold_right op init l
fold_left op (a :: l) init =
fold_right op init (a :: l) all: simpl.
4f
init = init
54
fold_left op l (op init a) =
op a (fold_right op init l) all: intros.
59
    -
5a reflexivity.
    -
54
5e rewrite <- IHl.
54
fold_left op l (op init a) =
op a (fold_left op l init) rewrite init_comm'.
54
op a (fold_left op l init) =
op a (fold_left op l init)
      reflexivity.
  Qed.
End Folds.