From 9c713f5d35ded9349e74acbd7721036aa794c37a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sat, 25 Jan 2025 19:37:20 +0100
Subject: [PATCH] wip

---
 tests/OK/FOL.lp  |  7 +++-
 tests/OK/Prop.lp | 34 ++++++++++++++++---
 tests/OK/Set.lp  |  6 ++--
 tests/OK/why3.lp | 86 ++++++++++++++++--------------------------------
 4 files changed, 68 insertions(+), 65 deletions(-)

diff --git a/tests/OK/FOL.lp b/tests/OK/FOL.lp
index a88b96dc1..a6c7277e2 100644
--- a/tests/OK/FOL.lp
+++ b/tests/OK/FOL.lp
@@ -4,7 +4,10 @@ require open tests.OK.Set tests.OK.Prop;
 
 // Universal quantification
 
-constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall
+constant symbol ∀ [a] : (τ a → Prop) → Prop;
+
+builtin "all" ≔ ∀;
+notation ∀ quantifier; // !! or \forall
 
 rule π (∀ $f) ↪ Π x, π ($f x);
 
@@ -12,6 +15,8 @@ rule π (∀ $f) ↪ Π x, π ($f x);
 
 constant symbol ∃ [a] : (τ a → Prop) → Prop; notation ∃ quantifier; // ?? or \exists
 
+builtin "ex" ≔ ∃;
+
 constant symbol ∃ᵢ [a] p (x:τ a) : π (p x) → π (∃ p);
 symbol ∃ₑ [a] p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;
 
diff --git a/tests/OK/Prop.lp b/tests/OK/Prop.lp
index 5c8e28ffa..0c3e10118 100644
--- a/tests/OK/Prop.lp
+++ b/tests/OK/Prop.lp
@@ -14,17 +14,25 @@ builtin "P" ≔ π;
 
 constant symbol ⊤ : Prop; // \top
 
+builtin "top" ≔ ⊤;
+
 constant symbol ⊤ᵢ : π ⊤;
 
 // false
 
 constant symbol ⊥ : Prop; // \bot
 
+builtin "bot" ≔ ⊥;
+
 constant symbol ⊥ₑ [p] : π ⊥ → π p;
 
 // implication
 
-constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // =>
+constant symbol ⇒ : Prop → Prop → Prop;
+
+builtin "imp" ≔ ⇒;
+
+notation ⇒ infix right 5; // =>
 
 rule π ($p ⇒ $q) ↪ π $p → π $q;
 
@@ -32,9 +40,15 @@ rule π ($p ⇒ $q) ↪ π $p → π $q;
 
 symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg
 
+builtin "not" ≔ ¬;
+notation ¬ prefix 100;
+
 // conjunction
 
-constant symbol ∧ : Prop → Prop → Prop; notation ∧ infix left 7; // /\ or \wedge
+constant symbol ∧ : Prop → Prop → Prop; // /\ or \wedge
+
+builtin "and" ≔ ∧;
+notation ∧ infix left 7;
 
 constant symbol ∧ᵢ [p q] : π p → π q → π (p ∧ q);
 symbol ∧ₑ₁ [p q] : π (p ∧ q) → π p;
@@ -42,11 +56,21 @@ symbol ∧ₑ₂ [p q] : π (p ∧ q) → π q;
 
 // disjunction
 
-constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6; // \/ or \vee
+constant symbol ∨ : Prop → Prop → Prop; // \/ or \vee
+
+builtin "or" ≔ ∨;
+
+notation ∨ infix left 6;
+assert x y z ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z);
 
 constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
 constant symbol ∨ᵢ₂ [p q] : π q → π (p ∨ q);
 symbol ∨ₑ [p q r] : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;
 
-// check that priorities are correctly set
-assert x y z ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z);
+// equivalence
+
+symbol ⇔ x y ≔ x ⇒ y ∧ y ⇒ x;
+
+builtin "eqv" ≔ ⇔;
+
+notation ⇔ infix right 30;
diff --git a/tests/OK/Set.lp b/tests/OK/Set.lp
index 91d93d140..ca7ba33f7 100644
--- a/tests/OK/Set.lp
+++ b/tests/OK/Set.lp
@@ -6,6 +6,8 @@ injective symbol τ : Set → TYPE; // `t or \tau
 
 builtin "T" ≔ τ;
 
-symbol ↦ : Set → Set → Set; notation ↦ infix 20;
+symbol ⤳ : Set → Set → Set; // \leadsto
 
-rule τ($a ↦ $b) ↪ τ $a → τ $b;
+notation ⤳ infix 20;
+
+rule τ($a ⤳ $b) ↪ τ $a → τ $b;
diff --git a/tests/OK/why3.lp b/tests/OK/why3.lp
index 23a34e44c..3c88ab234 100644
--- a/tests/OK/why3.lp
+++ b/tests/OK/why3.lp
@@ -1,61 +1,33 @@
-require open tests.OK.logic;
-require open tests.OK.natural;
+require open tests.OK.Prop tests.OK.Set tests.OK.FOL;
 
 prover "Alt-Ergo";
 prover_timeout 2;
 
-opaque symbol tautology : Π (a : Prop), P a → P a
-≔ begin
-    why3;
-end;
-
-opaque symbol thm_and1 : Π (a b : Prop), P ({|and|} a b) → P a
-≔ begin
-    why3;
-end;
-
-opaque symbol thm_and2 : Π (a b : Prop), P ({|and|} a b) → P b
-≔ begin
-    why3;
-end;
-
-opaque symbol excluded_middle : Π (a : Prop), P (or a (not a))
-≔ begin
-    why3;
-end;
-
-opaque symbol thm_or1 : Π (a b : Prop), P a → P (or a b)
-≔ begin
-    why3;
-end;
-
-opaque symbol thm_or2 : Π (a b : Prop), P b → P (or a b)
-≔ begin
-    why3;
-end;
-
-opaque symbol thm_imp : Π (a b : Prop), P (imp a b) → P a → P b
-≔ begin
-    why3;
-end;
-
-symbol o : U;
-rule T o ↪ Prop;
-
-constant symbol nat: U;
-symbol even (_: T nat): Prop;
-
-/*opaque symbol thm_ex : P (ex o (λ p: T o, imp p p))
-≔ begin 
-  why3;
-end;*/
-
-opaque symbol thm_even : P (ex nat (λ n: T nat, imp (even n) (even n)))
-≔ begin
-  why3;
-end;
-
-opaque symbol tyvar (a: U) (q: T a → T o): P (ex a (λ n: T a, imp (q n) (q n)))
-≔ begin
-  why3;
-end; 
+opaque symbol test1 p : π p → π p ≔ begin why3 end;
+
+opaque symbol test2 p q : π (p ∧ q) → π p ≔ begin why3 end;
+
+opaque symbol test3 : Π p q, π (p ∧ q) → π p ≔ begin why3 end;
+
+opaque symbol test4 p : π (p ∨ ¬ p) ≔ begin why3 end;
+
+opaque symbol test5 p q : π p → π (p ∨ q) ≔ begin why3 end;
+
+opaque symbol test6 p q : π (p ⇒ q) → π p → π q ≔ begin why3 end;
+
+constant symbol nat:Set;
+
+symbol even : τ nat → Prop;
+
+opaque symbol test7 : π (`∃ n, even n ⇒ even n) ≔ begin why3 end;
+
+opaque symbol test8 a p: π (`∃ x:τ a, p x ⇒ p x) ≔ begin why3 end;
+
+opaque symbol test9 a p : π (¬ (`∃ x:τ a, p x) ⇔ (`∀ x, ¬ (p x))) ≔ begin why3 end;
+
+//constant symbol o:Set;
+//rule τ o ↪ Prop;
+
+//opaque symbol test10 a (p:τ(nat ⤳ o)) : π (¬ (`∃ x:τ a, p x) ⇔ (`∀ x, ¬ (p x))) ≔ begin why3 end;
+
+//opaque symbol test10 : π (`∃ p, p ⇒ p) ≔ begin why3 end;