From 163f2c13937fc8539d6f71bc7ae789c2311ee1d4 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sat, 21 Mar 2020 11:32:09 +0100
Subject: [PATCH] new directory structure
- lambdapi.pkg
- no cert_f subfolder everywhere
---
README.md | 4 +---
adlib/{cert_f => }/bootstrap.lp | 2 +-
adlib/{cert_f => }/induction.lp | 4 ++--
adlib/{cert_f => }/nat.lp | 0
adlib/{cert_f => }/subtype.lp | 4 ++--
{adlib => alternatives/adlib}/core/nat.lp | 0
{adlib => alternatives/adlib}/core/nat_ops.lp | 0
.../prelude}/core/boolean_props.lp | 0
.../prelude}/core/booleans.lp | 0
.../prelude}/core/equalities.lp | 0
.../prelude}/core/if_def.lp | 0
.../prelude}/core/notequal.lp | 0
.../prelude}/core/quantifier_props.lp | 0
.../prelude}/core/xor_def.lp | 0
{sandbox => alternatives/sandbox}/core/rat.lp | 0
.../sandbox}/core/rat_explicit.lp | 0
lambdapi.pkg | 2 ++
prelude/{cert_f => }/functions.lp | 8 ++++----
prelude/{cert_f => }/logic.lp | 15 ++++++---------
prelude/{cert_f => }/numbers.lp | 17 ++++++++++++-----
sandbox/{cert_f => }/even.lp | 0
sandbox/{cert_f => }/rat.lp | 0
22 files changed, 30 insertions(+), 26 deletions(-)
rename adlib/{cert_f => }/bootstrap.lp (95%)
rename adlib/{cert_f => }/induction.lp (77%)
rename adlib/{cert_f => }/nat.lp (100%)
rename adlib/{cert_f => }/subtype.lp (96%)
rename {adlib => alternatives/adlib}/core/nat.lp (100%)
rename {adlib => alternatives/adlib}/core/nat_ops.lp (100%)
rename {prelude => alternatives/prelude}/core/boolean_props.lp (100%)
rename {prelude => alternatives/prelude}/core/booleans.lp (100%)
rename {prelude => alternatives/prelude}/core/equalities.lp (100%)
rename {prelude => alternatives/prelude}/core/if_def.lp (100%)
rename {prelude => alternatives/prelude}/core/notequal.lp (100%)
rename {prelude => alternatives/prelude}/core/quantifier_props.lp (100%)
rename {prelude => alternatives/prelude}/core/xor_def.lp (100%)
rename {sandbox => alternatives/sandbox}/core/rat.lp (100%)
rename {sandbox => alternatives/sandbox}/core/rat_explicit.lp (100%)
create mode 100644 lambdapi.pkg
rename prelude/{cert_f => }/functions.lp (92%)
rename prelude/{cert_f => }/logic.lp (87%)
rename prelude/{cert_f => }/numbers.lp (92%)
rename sandbox/{cert_f => }/even.lp (100%)
rename sandbox/{cert_f => }/rat.lp (100%)
diff --git a/README.md b/README.md
index 6fa3d64..61186d6 100644
--- a/README.md
+++ b/README.md
@@ -23,9 +23,7 @@ library, also known as _Prelude_. The prelude is available
- `prelude` contains parts of the PVS prelude
- `sandbox` contains miscellaneous experiments
- `tools` contains some additional scripts and utilities
-
-Each directory contains a directory per encoding, so the logic file for the
-prelude encoded with `cert_f` is under `prelude/cert_f/logic.lp`.
+- `alternativs` contains files in other encodings
## Emacs abbreviations
The `.dir-locals.el` activates the `abbrev-mode` when opening a Dedukti file,
diff --git a/adlib/cert_f/bootstrap.lp b/adlib/bootstrap.lp
similarity index 95%
rename from adlib/cert_f/bootstrap.lp
rename to adlib/bootstrap.lp
index 698dfa8..c0cef1a 100644
--- a/adlib/cert_f/bootstrap.lp
+++ b/adlib/bootstrap.lp
@@ -1,4 +1,4 @@
-require open encodings.cert_f
+require open personoj.encodings.cert_f
definition bool ≔ uProp
definition false ≔ prod bool (λ x, x)
diff --git a/adlib/cert_f/induction.lp b/adlib/induction.lp
similarity index 77%
rename from adlib/cert_f/induction.lp
rename to adlib/induction.lp
index 6d7e787..932f63b 100644
--- a/adlib/cert_f/induction.lp
+++ b/adlib/induction.lp
@@ -1,5 +1,5 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
// Allows to make case disjunction in proofs,
// [refine disjunction P ?Cfalse ?Ctrue]
diff --git a/adlib/cert_f/nat.lp b/adlib/nat.lp
similarity index 100%
rename from adlib/cert_f/nat.lp
rename to adlib/nat.lp
diff --git a/adlib/cert_f/subtype.lp b/adlib/subtype.lp
similarity index 96%
rename from adlib/cert_f/subtype.lp
rename to adlib/subtype.lp
index ec0d4d1..534f6e3 100644
--- a/adlib/cert_f/subtype.lp
+++ b/adlib/subtype.lp
@@ -1,5 +1,5 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
// rule Term (ePsub &A _ ⊑ &A) → Term true
// and Term ((ePsub &A &P) ⊑ (ePsub &B &Q)) →
diff --git a/adlib/core/nat.lp b/alternatives/adlib/core/nat.lp
similarity index 100%
rename from adlib/core/nat.lp
rename to alternatives/adlib/core/nat.lp
diff --git a/adlib/core/nat_ops.lp b/alternatives/adlib/core/nat_ops.lp
similarity index 100%
rename from adlib/core/nat_ops.lp
rename to alternatives/adlib/core/nat_ops.lp
diff --git a/prelude/core/boolean_props.lp b/alternatives/prelude/core/boolean_props.lp
similarity index 100%
rename from prelude/core/boolean_props.lp
rename to alternatives/prelude/core/boolean_props.lp
diff --git a/prelude/core/booleans.lp b/alternatives/prelude/core/booleans.lp
similarity index 100%
rename from prelude/core/booleans.lp
rename to alternatives/prelude/core/booleans.lp
diff --git a/prelude/core/equalities.lp b/alternatives/prelude/core/equalities.lp
similarity index 100%
rename from prelude/core/equalities.lp
rename to alternatives/prelude/core/equalities.lp
diff --git a/prelude/core/if_def.lp b/alternatives/prelude/core/if_def.lp
similarity index 100%
rename from prelude/core/if_def.lp
rename to alternatives/prelude/core/if_def.lp
diff --git a/prelude/core/notequal.lp b/alternatives/prelude/core/notequal.lp
similarity index 100%
rename from prelude/core/notequal.lp
rename to alternatives/prelude/core/notequal.lp
diff --git a/prelude/core/quantifier_props.lp b/alternatives/prelude/core/quantifier_props.lp
similarity index 100%
rename from prelude/core/quantifier_props.lp
rename to alternatives/prelude/core/quantifier_props.lp
diff --git a/prelude/core/xor_def.lp b/alternatives/prelude/core/xor_def.lp
similarity index 100%
rename from prelude/core/xor_def.lp
rename to alternatives/prelude/core/xor_def.lp
diff --git a/sandbox/core/rat.lp b/alternatives/sandbox/core/rat.lp
similarity index 100%
rename from sandbox/core/rat.lp
rename to alternatives/sandbox/core/rat.lp
diff --git a/sandbox/core/rat_explicit.lp b/alternatives/sandbox/core/rat_explicit.lp
similarity index 100%
rename from sandbox/core/rat_explicit.lp
rename to alternatives/sandbox/core/rat_explicit.lp
diff --git a/lambdapi.pkg b/lambdapi.pkg
new file mode 100644
index 0000000..8c92627
--- /dev/null
+++ b/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name = personoj
+root_path = personoj
diff --git a/prelude/cert_f/functions.lp b/prelude/functions.lp
similarity index 92%
rename from prelude/cert_f/functions.lp
rename to prelude/functions.lp
index 5d25812..a2f29e7 100644
--- a/prelude/cert_f/functions.lp
+++ b/prelude/functions.lp
@@ -1,7 +1,7 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-prelude.cert_f.logic
-require adlib.cert_f.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+personoj.prelude.logic
+require personoj.adlib.subtype as S
//
// functions [D, R: TYPE]
diff --git a/prelude/cert_f/logic.lp b/prelude/logic.lp
similarity index 87%
rename from prelude/cert_f/logic.lp
rename to prelude/logic.lp
index 18ee520..ef6be71 100644
--- a/prelude/cert_f/logic.lp
+++ b/prelude/logic.lp
@@ -1,7 +1,7 @@
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-require adlib.cert_f.induction as I
-require adlib.cert_f.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+require personoj.adlib.induction as I
+require personoj.adlib.subtype as S
//
// Booleans
@@ -28,7 +28,6 @@ symbol if {T: Term uType}: Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
//
// boolean_props
// Slightly modified from the prelude
-// FIXME explicitness required
constant symbol bool_exclusive: Term (neq false true)
constant symbol bool_inclusive A: Term ((eq A false) ∨ (eq A true))
@@ -46,15 +45,13 @@ qed
//
// xor_def
//
-// FIXME explicitness required
definition xor (a b: Term bool) ≔ neq a b
-// FIXME explicitness required
theorem xor_def (a b: Term bool):
- Term (@eq bool (xor a b) (if a (bnot b) b))
+ Term (eq (xor a b) (if a (bnot b) b))
proof
refine I.disjunction
- (λa: Term bool, @forall bool (λb, eq (xor a b) (if a (bnot b) b)))
+ (λa: Term bool, forall (λb, eq (xor a b) (if a (bnot b) b)))
?Cf ?Ct
refine I.disjunction
(λ b, eq (xor false b) (if false (bnot b) b))
diff --git a/prelude/cert_f/numbers.lp b/prelude/numbers.lp
similarity index 92%
rename from prelude/cert_f/numbers.lp
rename to prelude/numbers.lp
index 42ba6f7..a471a2a 100644
--- a/prelude/cert_f/numbers.lp
+++ b/prelude/numbers.lp
@@ -1,8 +1,7 @@
-require adlib.cert_f.subtype as S
-require open encodings.cert_f
-adlib.cert_f.bootstrap
-// adlib.cert_f.numerals
-prelude.cert_f.logic
+require personoj.adlib.subtype as S
+require open personoj.encodings.cert_f
+personoj.adlib.bootstrap
+personoj.prelude.logic
//
// Theory numbers
@@ -58,6 +57,8 @@ symbol closed_plus_real: ∀(x y: Term real),
let ynf ≔ ↑ numfield pr y in
Term (real_pred (xnf + ynf))
+hint Term &x ≡ Univ Type → &x ≡ uType
+
// With polymorphic plus
rule ty_plus real real → real
@@ -92,6 +93,12 @@ proof
refine S.restr real rational_pred
qed
+hint Psub &x ⊑ &y ≡ rational ⊑ real → &x ≡ rational_pred, &y ≡ real
+theorem rat_is_real_auto: Term (rational ⊑ real)
+proof
+ apply S.restr _ _
+qed
+
definition nonzero_rational_pred (x: Term rational): Term bool ≔
neq zero (↑ real rat_is_real x)
definition nonzero_rational ≔ Psub nonzero_rational_pred
diff --git a/sandbox/cert_f/even.lp b/sandbox/even.lp
similarity index 100%
rename from sandbox/cert_f/even.lp
rename to sandbox/even.lp
diff --git a/sandbox/cert_f/rat.lp b/sandbox/rat.lp
similarity index 100%
rename from sandbox/cert_f/rat.lp
rename to sandbox/rat.lp
--
GitLab