aa755

moved to https://aa755.github.io/decoding-human-body/ivermectin/2021/07/05/ivmrebuttal.html

aa755

(** tries to reverse engineer FPL billing algorithm: given x watt consumption what should be the bill?
the bill is printed in cents.
it comes within 100cents in the test cases
but doesnt exactly match, even though all computations except the last one to print in decimal (error < 1 cent) are exact.
*)

Require Import QArith.
Require Import Coq.Classes.DecidableClass.
Definition Qmax (a b:Q) : Q :=
  if ((Qle_bool a b)) then b else a.

aa755

Require Import List.
Import ListNotations.
Require Import ssreflect.
Lemma test1 :
  length ([1] ++ [2]) = 2 ->
  2 = 4.
Proof.
  intros HA.
  evar (N : nat).
  Unshelve.

aa755

  Axiom natMod7: Type.
  Axiom inj : nat -> natMod7.

Inductive Vector : natMod7 → Prop :=
| ttrue  : Vector (inj 0)
| ffalse : False -> Vector (inj 7).

Lemma eqq:  inj 7 = inj 0. Proof. Admitted.

Lemma ff: False.

aa755

coq@99313f5cc7b0:~/aac-tactics$ git log --stat
commit 8ba7a8b2c5ce80859e9645c89ebe39c33948525c (HEAD -> master, origin/master, origin/HEAD)
Author: Karl Palmskog <palmskog@gmail.com>
Date:   Fri Jun 21 00:04:44 2024 +0200

    silence warning 67 in Dune build

 src/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)