From f41a2c1cabade288798721cd3564887662043fab Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Sat, 28 Sep 2024 14:57:26 +0100 Subject: [PATCH] README: minor typos, strip axiom --- README.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index a8ccb8a..c7bb5a4 100644 --- a/README.md +++ b/README.md @@ -6,9 +6,9 @@ The name _bonak_ comes from an imaginary monster in Daisy Johnson's novel [Every Some features of this project: -1. We do not make use of [HoTT](https://github.com/HoTT/HoTT), or any fancy libraries for that matter. Bonak is written is vanilla Coq, making use of the core standard libarary. In particular, we make heavy use of [SProp](https://coq.inria.fr/refman/addendum/sprop.html) for proof irrelevance. +1. We do not make use of [HoTT](https://github.com/HoTT/HoTT), or any fancy libraries for that matter. Bonak is written is vanilla Coq, making use of the core standard library. In particular, we make heavy use of [SProp](https://coq.inria.fr/refman/addendum/sprop.html) for definitional proof irrelevance. 2. Bonak has led to many bugs being filed and fixed in core Coq. It pushes the boundaries of proof assistant technology, and can serve as a benchmark against which to improve core Coq features. -3. As the main contribution of Bonak is the Coq code, we have placed high emphasis on code cleanliness and readability. As a result, it's quite plesant to step through the code, and have a succinct goal at all times. +3. As the main contribution of Bonak is the Coq code, we have placed high emphasis on code cleanliness and readability. As a result, it's quite pleasant to step through the code, and have a succinct goal at all times. 4. Bonak is tiny! In ~800 lines of Coq code, we have managed to prove something remarkable. We did have a lot of false starts, and tried various approaches, before settling on what we have today. Our axioms are: @@ -20,9 +20,6 @@ Axioms: functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g -fext_computes - : forall (A : Type) (B : A -> HSet) (f : forall a : A, B a), - functional_extensionality_dep f f (fun a : A => eq_refl) = eq_refl ``` ## Current status