Abhishek Anand aa755

General Coq Background

This is a Coq programming task. First, some general guidelines about Coq programming tasks.

Admitting holes (defer less critical/important parts)

Complex Coq programs are often written incrementally. Coq allows us to "admit" helper functions temporarily so that they can be defined later. However, in that case, you need to come up with the type of the helper function. For example, you can admit a helper function to convert a Z to a string, as follows:

	coq@99313f5cc7b0:~/aac-tactics$ git log --stat
	commit 8ba7a8b2c5ce80859e9645c89ebe39c33948525c (HEAD -> master, origin/master, origin/HEAD)
	Author: Karl Palmskog <[email protected]>
	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(-)

	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.

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

	(** 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.