Tally.Laws

Laws

What total, append and size guarantee. Theorems whose comment opens with a bold line appear on the Guarantees page.

From Tally Require Import Core.
Open Scope tally_scope.

Arithmetic

✓ No axioms

Addition regroups.

Lemma add_regroup (a b c : nat) : a + b + c = a + (b + c).

Qed

Proof.
  induction a as [| a IH].
  - reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

References

Uses

Used by

total_append

Appending

✓ No axioms

Appending adds totals.

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

Arguments

a : tally

the counts that come first.

b : tally

the counts that come last.

Theorem total_append (a b : tally) : total (append a b) = total a + total b.

Arguments

a : tally

the counts that come first.

b : tally

the counts that come last.

Qed

Proof.
  induction a as [| n rest IH].
  - reflexivity.
  - simpl. rewrite IH. symmetry. apply add_regroup.
Qed.

References

Uses

Used by

total_append_empty

✓ No axioms

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.

Qed

Proof.
  apply total_append.
Qed.

References

Uses

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.

References

Uses

Used by

size_stable

Rests on Laws.counts_are_small

Size is stable.

Rests on the assumption above, so its badge reads as axiom-dependent.

Theorem size_stable (t : tally) : size t = size t.

Qed

Proof.
  exact (counts_are_small t).
Qed.

References

Uses

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 Not proved

Admitted.

References

Uses

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).

Qed

Proof.
  discriminate.
Qed.

References

Uses

✓ No axioms

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.

Qed

Proof.
  reflexivity.
Qed.

References

Uses