alethelf.lp

require open Stdlib.FOL;
require open Stdlib.Prop;
require open Stdlib.Set;
require open Stdlib.Nat;
require open Stdlib.Bool;
require open Stdlib.Eq;
require open Stdlib.Z;
require open Stdlib.List;

// References use
// https://github.com/SMT-LIB/SMT-LIB.github.io/blob/2c5ae03b491c8c66e3570ad5f96940e585ee79c9/Version3/Core.smt3
// https://smtlib.cs.uiowa.edu/version3.shtml
// https://github.com/cvc5/alfc/blob/main/user_manual.md

/*
(declare-type Bool () :builtin
"The (binary) set {true, false}")
*/
// symbol : Prop;


/*
; Equality  
  (declare-const = (-> (! Type :var A :implicit) 
                       A A Bool)
   :chainable 
   :builtin 
   "= denotes the identity function, which returns true iff 
    its two arguments are identical.")
*/
// constant symbol = : Π [a: Set], τ a → τ a → Prop;

// (define-const true Bool)
// (declare-const false Bool)


// (declare-type BitVec ((! Int :var m :restrict (> m 0)))
// In PVS [n: {m : Int | m > 0} → BitVec(n) → BitVec(n)]
symbol BitVec (m: ℤ) (p: π (0 < m)): TYPE;

print  BitVec;

// (declare-const div (→ Int (! Int :var n :restrict (distinct n 0)) Int)
symbol div (n: ℤ) (p: π (n ≠ 0)): TYPE;



// (declare-type Vector (Type (! Int :var m :restrict (>= m 0)))
symbol Vector (m: ℤ) (p: π (0 ≤ m)): TYPE;
//(define-type RVector ((n Int :restrict (> n 0))) (Vector Real n))
symbol RVector (n: ℤ) (p: π (0 < n)): TYPE;

// (define-type RV8 () (RVector 8))
opaque symbol prf : π (0 < 8) ≔
begin
    simplify; apply top;
end;

// but we can inline the proof of π (0 < 8)
symbol RV8: RVector 8 top;


/*
Module could be simulated with Lambdapi Module. Each module will need to have its own file.
Lambdapi does not support companion module (module in module).

(define-module M
   (
    (declare-type A ())    (declare-type B ())     (declare-type C ()) 
    (declare-const a A)    (declare-const b B)
    (declare-const f (→ A B))
    (declare-const g (→ B A)) 
    (define-const  h (→ A A) (lambda ((x A)) (g (f x))))
    (declare-const c (→ A C))
   )
   :types ( (A Type) (B Type) )
   :consts ( (a A) (f (→ A B)) (h (→ A A)) )
)
In the example above, only two of the type constructors and three of the constants are exported. 
Modifier `private` could prefix all symbol that are not in :types and :consts in a Lambdapi Module.


(declare-const a1 M1::A) ; declares a1 in the top-level namespace
(assert (= a1 M1::a))    ; adds this equality to the assertion context
(open M1)

(declare-const a1 M1::A) will be translate into `symbol a1: M1.A;`
(open M1) will be translate into `open M1;`
*/

/*
(define-inductive-types 
    ((Size ()) (BinTree ()) (Option (Type)) (List (Type)) (Pair (Type Type)))
    ( ; Size
      ( (small Size)
        (medium Size)
        (large Size)
      )
      ; BinTree
      ( (empty BinTree)
        (node (-> (! BinTree :selector left) (! BinTree :selector right) BinTree))
      )
      ; Option
      ( (none (→ (! Type :var A)   ; Type input is explicit for this constructor
                 (Option A)))    
        (some (→ (! Type :var A :implicit) 
                 (! A :selector val) (Option A)))
      )
      ; List
      ( (nil (→ (! Type :var E)    ; Type input is explicit
                (List E))) 
        (cons (→ (! Type :var E :implicit) 
                   (! E :selector head) (! (List E) :selector tail)) (List E))
      )
      ; Pair
      ( (pair (→ (! Type :var A :implicit) (! Type :var B :implicit) 
                 (A :selector first) (B :selector second) (Pair A B))))
      )
    )
  )

The command define-inductive-types takes two arguments:

1. a list of pairs of consisting of a type constructor (the name of the inductive type) and a possibly empty list of the form (Type ... Type)
    for each type constructor, indicating the number of type parameters it takes;
2. a corresponding list of value constructors for each inductive type.

The value constructors for an inductive type are themselves grouped in a list.
Each element of this list is a pair of a constructor and its type.
The type is given with the same syntax as any other (possibly functional) type.
An optional :selector attribute for one of the arguments of the constructor can be used to name the corresponding selector.

Several constraints on the type definition ensure the generality and the well-foundedness of the type.

* If a datatype D being defined has n parameters, each constructor of that datatype must return a value whose type has the form (D X₁ ... Xᵢ)
where X₁ ... Xᵢ are i distinct type variables. Consequently, the constructor must have those type variables as (implicit or explicit) input parameters.

* An inductive type can be parametrized by other types but not values. So it can be polymorphic but not dependent in general.

* If a datatype D being defined has n parameters, each constructor of that datatype must return a value whose type has the form (D X₁ ... Xᵢ)
where X₁ ... Xᵢ are i distinct type variables. Consequently, the constructor must have those type variables as (implicit or explicit) input parameters.
The constructors of the the same datatype must have distinct names. However, the same name can be used for two constructors of distinct inductive types.

* An inductive type can be parametrized by other types but not values.
So it can be polymorphic but not dependent in general.
This is a temporary restriction that may be lifted at a later time.

* No nested types are allowed. That is, the type of a constructor's argument for an inductive type D cannot be a type term that nests D
within another type constructor. For instance, it is not possible to define a parametric inductive type (Tree A) with a constructor of type
(→ A (List (Tree A)) (Tree A)) or (→ A (Array Int (Tree A)) (Tree A)) because (Tree A) occurs nested in List (resp. Array).

* The same well-foundedness constraints as in 2.6 (which enable the type inhabited).
*/

/*
   All Well-foundedness properties of SMTLIB3 inductive type might not be checked by Lambdapi type checker.
   It is something we have to verify.
*/

inductive Size: TYPE ≔
| small: Size
| medium: Size
| large: Size;

print 𝕃;

(A: Set) inductive Option: TYPE ≔
| None : Option A
| Some : τ A  → Option A;

print Option;
/*
Argument `A` is already made implicit.

constant symbol Option : Set → TYPE;
constant symbol None : Π [a: Set], Option a;
constant symbol Some : Π [a: Set], τ a → Option a;
*/

// (define-inductive-type (List (Type)) 
// ( (nil (→ (! Type :var E) (List E))) 
//   (cons (→ (! Type :var E :implicit) 
//            (! E :sel head) (! (List E) :sel tail)) (List E))
// )
// )

// The second new command, provides a light-weight syntax for datatypes that have only constant constructors, as in:
// (define-enumeration-type Size (small medium large))
// This is similar as
// (define-inductive-types ( (Size ()) )
// ( ((small Size) (medium Size) (large Size)) )
// )

// # Right/Left associative with nil terminator

// (declare-const or (-> Bool Bool Bool) :right-assoc)
symbol or: Prop → Prop → Prop;
//notation or infix right 2;
rule or (or $x $y) $z ↪ or $x (or $y $z);


// (declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
symbol ornil: Prop → Prop → Prop;
//notation ornil infix right 2;
// rule ornil $x ↪ (ornil) $x ⊥;

// It is not possible to simulate `:right-assoc-nil false` by RW because type are not preserved.

// Or to have two symbols.
symbol or-unary: Prop → Prop;
rule or-unary $x ↪ (or) $x ⊥;

// # Chainable
// (declare-const >= (-> Int Int Bool) :chainable)
// use list...

// # Pairwise
// (declare-const distinct (-> (! Type :var T :implicit) T T Bool) :pairwise and)
// In the above example, (distinct x y z) is syntax sugar for (and (distinct x y) (distinct x z) (distinct y z)).


// (declare-sort Int 0)
// (declare-consts <numeral> Int)
// (declare-type BitVec (Int))

// (declare-const concat (->
//   (! Int :var n :implicit)
//   (! Int :var m :implicit)
//   (BitVec n)
//   (BitVec m)
//   (BitVec (alf.add n m))))

symbol <_compat_< x y : π (0 < x ⇒ 0 < y ⇒ 0 < x + y) ≔
begin admit end;

symbol concat n m 
(p: π (0 < n)) (q: π (0 < m))
(b1: BitVec n p) (b2: BitVec m q): BitVec (n + m) (<_compat_< n m p q);


// (declare-fun x () (BitVec 2))
// (declare-fun y () (BitVec 3))
// (define-fun z () (BitVec 5) (concat x y))
symbol x: BitVec 2 top;
symbol y: BitVec 3 top;
symbol z : BitVec 5 (<_compat_< 2 3 top top) ≔ concat 2 3 top top x y;


// Declaring Proof Rules

// (declare-const = (-> (! Type :var T :implicit) T T Bool))
// (declare-rule refl ((T Type) (t T))
//     :premises ()
//     :args (t)
//     :conclusion (= t t)
// )
constant symbol = [a] : τ a → τ a → Prop;
constant symbol refl [a] (t:τ a) : π (= t t);

// (declare-const = (-> (! Type :var T :implicit) T T Bool))
// (declare-rule symm ((T Type) (t T) (s T))
//     :premises ((= t s))
//     :conclusion (= s t)
// )
constant symbol sym [a] (t:τ a) (s:τ a) : π (= t s) → π (= s t);

// (declare-fun >= (Int Int) Bool)
// (declare-rule leq-contra ((x Int))
//     :premise ((>= x 0))
//     :requires (((alf.is_neg x) true))
//     :conclusion false)
symbol ≥:  ℤ → ℤ → Prop;
symbol leq-contra
    (x: ℤ)                  // ((x Int))
    (requires1: π (x < 0))  // :requires (((alf.is_neg x) true))  -- Something we need to verify ?
    : π (≥ x 0)             // :premise ((>= x 0)) -- Witness in a previous step
        → π ⊥;              // :conclusion false

// (sig A P), or more suggestively {x:A | P x},
// denotes the subset of elements of the type A which satisfy the predicate P.
// In Coq it is defined as:s
// Inductive sig (A:Type) (P:A -> Prop) : Type :=
// exist : forall x:A, P x -> sig P.
// symbol sig: Set → (Set → Prop) → Set;
// symbol exist: Π (x : Set), 
(a:Set) (P: τ a → Prop) inductive sig: TYPE ≔
exist x : π (P x) → sig a P;

symbol π₁ s p : sig s p → τ s;
rule π₁ _ _ (exist $x $y) ↪ $x;

// Suggestion: use Subsets and Sigma-types for (x T) :requires P
// We have then the following definition
symbol leq-contra'
    (x-subset : sig int (λ (u: τ int), u > 0))      // ((x Int)) :requires (((alf.is_neg x) true))
    : π (≥ (π₁ _ _ x-subset) 0)                     // :premise ((>= x 0))
    → π ⊥;                                          // :conclusion false


// # Match statements in ALF
// The ALF checker supports an operator alf.match for performing pattern matching on a target term. The syntax of this term is:

// The ALF language supports a command for defining ordered lists of rewrite rules
// that can be seen as computational side conditions. The syntax for this command is as follows.
// (program contains
//     ((l Bool) (x Bool) (xs Bool :list))
//     (Bool Bool) Bool
//     (
//         ((contains false l)     false)
//         ((contains (or l xs) l) true)
//         ((contains (or x xs) l) (contains l xs))
//     )
// )
//symbol o: Prop;

// (a:Prop) inductive premise-list : TYPE ≔
// | □ₚ : premise-list a // \Box
// | ⸬ₚ : π a → premise-list a → premise-list a;

//print premise-list;



// (declare-rule symm ((F Bool))
//     :premises (F)
//     :conclusion
//         (alf.match ((t1 Int) (t2 Int)) F
//             (
//                 ((= t1 t2)       (= t2 t1))
//                 ((not (= t1 t2)) (not (= t2 t1)))
//             )
//         )
// )
symbol symm (t1 t2: ℤ): Prop → Prop;
rule symm $x $y (= $x $y) ↪ = $x $y
with symm $x $y (¬ (= $x $y)) ↪ (¬ (= $y $x));

// alf.requires t1 t2 t3)
// Returns t3 if t1 is (syntactically) equal to t2, and is not evaluated otherwise.

constant symbol o : Set;
rule τ o ↪ Prop;
// (program mk_trans ((t1 Int) (t2 Int) (t3 Int) (t4 Int) (tail Bool :list))
//     (Int Int Bool) Bool
//     (
//         ((mk_trans t1 t2 (and (= t3 t4) tail)) (alf.requires t2 t3 (mk_trans t1 t4 tail)))
//         ((mk_trans t1 t2 true)                 (= t1 t2))
//     )
// )
//rule trans $t1 $t2 $t3 $t4 (= $x $y) ↪ = $x $y;

// (declare-rule trans (E Bool))
//     :premise-list E and
//     :conclusion
//         (alf.match ((t1 Int) (t2 Int) (tail Bool :list)) E
//         (
//             ((and (= t1 t2) tail) (mk_trans t1 t2 tail))
//         ))
// )


// When applying this rule, the formulas proven to this rule (say F1 ... Fn) will be collected
// and constructed as a single formula via the provided operator (and),
// and subsequently matched against the premise pattern F. In particular,
// in this case F is bound to (and F1 ... Fn). The conclusion of the rule returns F itself.
// Note that the type of functions provided as the second argument of :premise-list
// should be operators that are marked to take an arbitrary number of arguments,
// that is those marked e.g. with :right-assoc-nil or :chainable.
// The condition  :right-assoc-nil could not be check with Lambdapi, but :chainable comes for
// free with the type signature.
symbol premise-list : 𝕃 o → (Prop → Prop → Prop) → Prop;
rule premise-list ($x ⸬ $l) $op ↪ $op $x (premise-list $l $op)
with premise-list □ _ ↪ ⊤;

symbol a: Prop;
symbol b: Prop;
symbol c: Prop;
symbol d: Prop;

symbol eqab ≔ = a b;
symbol eqbc ≔ = b c;
symbol eqcd ≔ = c d;

symbol E ≔ (= a b) ⸬ (= b c) ⸬ (= c d) ⸬ □;

// alf.requires is an operator that evalutes to its third argument
// if and only if its first two arguments are equivalent. 
symbol alf-requires [a]:  τ a → τ a → τ a → τ a;
rule alf-requires $x $x $t ↪ $t;

assert ⊢ alf-requires a a ⊤ ≡ ⊤;
assert ⊢ alf-requires a b ⊤ ≡ alf-requires a b ⊤;

// The ALF language supports a command for defining ordered lists of rewrite rules
// that can be seen as computational side conditions. The syntax for this command is as follows.
// (declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
// (program contains
//     ((l Bool) (x Bool :list) (xs Bool :list))
//     (Bool Bool) Bool
//     (
//         ((contains false l)     false)
//         ((contains (or l xs) l) true)
//         ((contains (or x xs) l) (contains l xs))
//     )
// )
sequential symbol contains: Prop → Prop → Prop;
rule contains ⊥ _ ↪ ⊥
with contains (or $l $x) $l ↪ ⊤
with contains (or $x $xs) $l ↪ contains $l $xs;

// (program mk_trans ((t1 Int) (t2 Int) (t3 Int) (t4 Int) (tail Bool :list))
//     (Int Int Bool) Bool
//     (
//         ((mk_trans t1 t2 (and (= t3 t4) tail)) (alf.requires t2 t3 (mk_trans t1 t4 tail)))
//         ((mk_trans t1 t2 true)                 (= t1 t2))
//     )
// )
sequential symbol mk_trans [a] : τ a → τ a → Prop → Prop;
rule @mk_trans o $t1 $t2 ((@= o $t3 $t4) ∧ $tl) ↪ alf-requires $t2 $t3 (mk_trans $t1 $t4 $tl)
with @mk_trans o $t1 $t2 ⊤ ↪ = $t1 $t2;


// (declare-rule trans (E Bool))
//     :premise-list E and
//     :conclusion
//         (alf.match ((t1 Int) (t2 Int) (tail Bool :list)) E
//         (
//             ((and (= t1 t2) tail) (mk_trans t1 t2 tail))
//         ))
// )
symbol trans: Prop → Prop;
rule trans ((= $t1 $t2) ∧ $tl) ↪ mk_trans $t1 $t2 $tl;

compute trans (premise-list E (∧));


// let-expresions to applications 
// let x : t := b in v equiv to (fun x : t => v) b

// (alf.ite t1 t2 t3) Returns t2 if t1 evaluates to true, t3 if t2 evaluates to false,
// and is not evaluated otherwise. Note that the branches of this term are only evaluated if they are the return term.
sequential symbol ite: Prop → Prop → Prop → Prop;
rule ite ⊤ $t2 _ ↪ $t2
with ite ⊥ _ $t3 ↪ $t3;

// (alf.concat f t1 t2)
// If t1 is an f-list with children t11 ... t1n and t2 is an f-list with children t21 ... t2m,
// this returns (f t11 ... t1n t21 ... t2m) if n+m>0 and nil otherwise. Otherwise, this operator does not evaluate.

symbol alf-cons [a] (f: τ a → τ a → τ a) (t1 t2: τ a) ≔ f t1 t2;

//type alf-cons;

// (program list.intro
//     ((L Type) (cons (-> L L L)) (nil L) (intro-nil L) (x L) (xs L :list))
//     ((-> L L L) L L) L
//     (
//         ((list.intro cons nil (cons x xs)) (cons x xs))
//         ((list.intro cons nil nil)         nil)
//         ((list.intro cons nil x)           (alf.cons cons x nil))
//     )
// )
sequential symbol list-intro [L]: (τ L → τ L → τ L) → τ L  → τ L  → τ L;
rule list-intro ($op) $nil $op ↪ $op
with list-intro ($op) $nil $nil ↪ $nil
with list-intro $op $nil $x ↪ alf-cons $op $x $nil;


// ; remove cons c xs
// ; Removes the first occurrence of `c` from `xs`.
// (program nary.remove
//     ((L Type) (cons (-> L L L)) (nil L) (c L) (y L) (xs L :list))
//     ((-> L L L) L L L) L
//     (
//         ((nary.remove cons nil c (cons c xs)) xs)
//         ((nary.remove cons nil c (cons y xs)) (alf.cons cons y (nary.remove cons nil c xs)))
//         ((nary.remove cons nil c nil)         nil)
//     )
// )
sequential symbol nary-remove [L]: (τ L → τ L → τ L) → τ L  →  τ L  → τ L  → τ L;
rule nary-remove (or) $nil $c (or $c $xs) ↪ $xs //FIXME: HO-parttern 
with nary-remove (or) $nil $c (or $y $xs) ↪ alf-cons (or) $y (nary-remove or $nil $c $xs);


// (define removeSelf ((l Bool) (C Bool))
//     (alf.ite (alf.is_eq l C) false (nary.remove or false l C)))
symbol removeSelf (l C: Prop) ≔ ite (= l C) ⊥ (nary-remove or ⊥ l C);

symbol resolve: Prop →  Prop →  Prop →  Prop →  Prop;

type resolve;

// ; RESOLUTION
// (program resolve ((C1 Bool) (C2 Bool) (pol Bool) (L Bool))
//     (Bool Bool Bool Bool) Bool
//     (
//       ((resolve C1 C2 pol L)
//         (let ((lp (alf.ite pol L (not L))))
//         (let ((ln (alf.ite pol (not L) L)))
//             (alf.from_list or (alf.concat or
//                     (removeSelf lp (list.intro or false C1))
//                     (removeSelf ln (list.intro or false C2)))))))
//     )
// )

// (declare-rule resolution ((C1 Bool) (C2 Bool) (pol Bool) (L Bool))
//     :premises (C1 C2)
//     :args (pol L)
//     :conclusion (resolve C1 C2 pol L)
// )
symbol resolution [a b] (pol L: Prop) : π a → π b → Prop ≔ λ c1, λ c2, resolve a b pol L;

// ; CHAIN_RESOLUTION
// ; Applies multiple steps of resolution but leaves the first argument in n-ary form.
// (program chainResolveRec ((C1 Bool) (C2 Bool) (Cs Bool :list) (pol Bool) (L Bool) (args Bool :list))
//     (Bool Bool Bool) Bool
//     (
//         ((chainResolveRec C1 true true)              (alf.from_list or C1))
//         ((chainResolveRec C1 (and C2 Cs) (and pol L args))
//             (chainResolveRec
//                 (let ((lp (alf.ite pol L (not L))))
//                 (let ((ln (alf.ite pol (not L) L)))
//                     (alf.concat or
//                             (removeSelf lp C1)
//                             (removeSelf ln (alf.to_list or C2))))) Cs args))
//     )
// )

// ; This is a chain or resolution steps as described in the cvc5 proof rule
// ; documentation.
// ; `Cs` is a conjunction or the premise clauses.
// ; `args` is a conjunction where the alternating conjuncts are polarity and
// ;        pivot literal.
// (declare-rule chain_resolution ((Cs Bool) (args Bool))
//     :premise-list Cs and
//     :args (args)
//     :conclusion
//         (alf.match ((C1 Bool) (C2 Bool :list))
//             Cs
//             (((and C1 C2) (chainResolveRec (alf.to_list or C1) C2 args))))
//