The Tally project

-Q theories Tally

theories/Core.v
theories/Laws.v
theories/Prose.v

(**md # Core

A tally is a list of counts. This module defines the type and the two functions the rest of the
project reasons about: [`total`](Core.html#total) and [`append`](Core.html#append).
*)

(** A list of counts. *)
Inductive tally : Type :=
  | empty : tally
  | cons : nat -> tally -> tally.

Declare Scope tally_scope.
Delimit Scope tally_scope with tally.
Infix "::" := cons (at level 60, right associativity) : tally_scope.
Open Scope tally_scope.

(** The sum of every count in a tally.
    - [t:] the tally summed. *)
Fixpoint total (t : tally) : nat :=
  match t with
  | empty => 0
  | n :: rest => n + total rest
  end.

(**md The counts of `a`, followed by the counts of `b`.

- [a:] the counts that come first.
- [b:] the counts that come last. *)
Fixpoint append (a b : tally) : tally :=
  match a with
  | empty => b
  | n :: rest => n :: append rest b
  end.

(** How many counts a tally holds.
    - [t:] the tally measured. *)
Fixpoint size (t : tally) : nat :=
  match t with
  | empty => 0
  | _ :: rest => S (size rest)
  end.

From Tally Require Import Core.

(**md # Laws

What [`total`](Core.html#total), [`append`](Core.html#append) and [`size`](Core.html#size)
guarantee. Theorems whose comment opens with a bold line appear on the Guarantees page.
*)

Open Scope tally_scope.

(**md ## Arithmetic *)

(** Addition regroups. *)
Lemma add_regroup (a b c : nat) : a + b + c = a + (b + c).
Proof.
  induction a as [| a IH].
  - reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

(**md ## Appending *)

(**md
**Appending adds totals.**

The total of two tallies appended equals the sum of their totals.

- [a:] the counts that come first.
- [b:] the counts that come last.
*)
Theorem total_append (a b : tally) : total (append a b) = total a + total b.
Proof.
  induction a as [| n rest IH].
  - reflexivity.
  - simpl. rewrite IH. symmetry. apply add_regroup.
Qed.

(**md
**The empty tally changes nothing.**

Appending `empty` leaves the total as it was.
*)
Corollary total_append_empty (a : tally) : total (append a empty) = total a + 0.
Proof.
  apply total_append.
Qed.

(**md ## Assumed and unfinished *)

(** An assumption, which the badge on any theorem using it reports. *)
Axiom counts_are_small : forall t : tally, size t = size t.

(**md
**Size is stable.**

Rests on the assumption above, so its badge reads as axiom-dependent.
*)
Theorem size_stable (t : tally) : size t = size t.
Proof.
  exact (counts_are_small t).
Qed.

(**md
**Appending adds sizes.**

Not proved yet, so it sits in the Open group.
*)
Theorem size_append (a b : tally) : size (append a b) = size a + size b.
Admitted.

(**md
**The claim that all totals match is false.**

The name's `_falsified` suffix files this disproof in the Falsified group.
*)
Theorem totals_differ_falsified : total (1 :: empty) <> total (2 :: empty).
Proof.
  discriminate.
Qed.

(**md
**Generated tallies sum correctly.**

@checked with one thousand generated tallies, which files it in the Checks group.
*)
Theorem generated_sum : total (1 :: 2 :: empty) = 3.
Proof.
  reflexivity.
Qed.

From Tally Require Import Core.

(**md # Prose syntax

Every comment form the navigator reads. The documentation site quotes these comments and renders
them with the plugin's own code.
*)

(** * A doc comment heading

    One to four stars open a heading in a doc comment. *)

(** ** A second-level heading *)

(** A paragraph in a doc comment.
    Lines join into one paragraph, and a blank line starts the next.

    Square brackets mark code: [total] links to its declaration, and [1 + 1] stays plain code. *)
Definition doc_paragraphs := total empty.

(** - This dash is plain text, since doc comments have no lists: only headings, paragraphs and
    [code]. Use a Markdown comment for lists. *)
Definition doc_no_lists := 0.

(**md ## A Markdown heading

The `md` marker after the opening stars selects Markdown, with one to six `#` marks for a heading. *)

(**md **Bold**, *emphasis*, `total` as a linked name and `1 + 1` as plain code.

- A list item
- Another, with a [link to a declaration](Core.html#append)

| Form | Marker | Lists |
|---|---|---|
| Doc | none | no |
| Markdown | `md` | yes |

```text
A fenced block. `total` stays text here.
```

An external [link](https://rocq-prover.org), and raw HTML shown as text: <b>not bold</b>. *)
Definition markdown_forms := total empty.

(** Arguments in a doc comment.
    - [n:] the count added, whose entry
      continues on an indented line.
    - [t:] the tally extended, mentioning [size]. *)
Definition push (n : nat) (t : tally) : tally := cons n t.

(**md Arguments in a Markdown comment.

- [t:] the tally read, mentioning `append`. *)
Definition is_empty (t : tally) : bool :=
  match t with
  | empty => true
  | cons _ _ => false
  end.

(* A plain comment above a declaration documents it, as a doc comment does. *)
Definition with_plain_comment (* a comment inside the statement *) := 0.

(** A comment that has a line of its own, and is attached to no declaration, reads as prose between
    the declarations. *)

(**md
**A first line wholly in bold titles a theorem.**

A `Theorem` or `Corollary` with this form appears on the Guarantees page under that title. A `Lemma`
never does.
*)
Theorem titled_theorem : total empty = 0.
Proof.
  (* A plain comment inside a proof folds with the proof. *)
  reflexivity.
Qed.