cosmetic bugs + Lambdapi's Set is already computational category theory, should we extend with official support?

[1337777]

Mostly feedback on cosmetic issues + unavoidable question of Lambdapi's support for unfamiliar but novel proof assistants:

(1) the Deducteam/lambdapi-stdlib andDeducteam/lambdapi-logics are missing fundamental things such as Sigma Σ types over Set for both predicates in Set and predicates in Prop. This absence gives the wrong impression that there is some impossibility to express them within the Lambdapi type system or that it woud require hacks. By the way, the Sigma type alternative psub in Deducteam/lambdapi-logics/U/PredSub.lp I don't understand the motivation for this alternative formulation.

(2) the Deducteam/lambdapi-stdlib/blob/master/List.lp is missing fundamental things such as the foldl fold iterators, and the phrasing inside the file which says they are "Not available" gives the wrong impression that there is some impossibility to express them within the Lambdapi type system or that it woud require hacks. It should be made clear to what extend the Coq list library can be ported (for example, that fancy multifix notations would not work).

(3) For clarity that we are on the same page, here are examples for the previous 2 suggestions:

constant symbol Set : TYPE;
injective symbol τ : Set → TYPE;
builtin "T" ≔ τ;

constant symbol Prop : TYPE;
builtin "Prop" ≔ Prop;
injective symbol π : Prop → TYPE;
builtin "P" ≔ π;

constant symbol = [a] : τ a → τ a → Prop;
notation = infix 10;
constant symbol eq_refl [a] (x:τ a) : π (x = x);
constant symbol ind_eq [a] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
builtin "eq"    ≔ =;
builtin "refl"  ≔ eq_refl;
builtin "eqind" ≔ ind_eq;

constant symbol Π_ : Π [a], (τ a → Set) → Set; notation Π_ quantifier;
rule τ (@Π_ $a $b) ↪ Π x : τ $a, τ ($b x);

constant symbol →_ : Set → Set → Set; notation →_ infix right 10;
rule τ ($x →_ $y) ↪ τ $x → τ $y;

constant symbol × : Set → Set → Set; notation × infix right 10; 
symbol & [a b] : τ a → τ b → τ (a × b); notation & infix right 30;
symbol ₁ [a b] : τ(a × b) → τ a; notation ₁ postfix 10;
rule ($x & _)₁ ↪ $x;
symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10;
rule (_ & $x)₂ ↪ $x;

inductive τΣ_ [a : Set] (P : τ a → Set) : TYPE ≔
| Struct_sigma [a P] : Π
(sigma_Fst : τ a)
(sigma_Snd : τ (P sigma_Fst) ), @τΣ_ a P;
notation τΣ_ quantifier;
constant symbol Σ_ [a : Set] (P : τ a → Set) : Set; notation Σ_ quantifier;
rule τ (Σ_ $P) ↪ τΣ_ $P;
injective symbol sigma_Fst [a P] (s : @τΣ_ a P) : τ a;
rule sigma_Fst (Struct_sigma $1 $2) ↪ $1;
injective symbol sigma_Snd [a P] (s : @τΣ_ a P) : τ (P (sigma_Fst s)) ;
rule sigma_Snd (Struct_sigma $1 $2) ↪ $2;

inductive τsub_ [a : Set] (P : τ a → Prop) : TYPE ≔
| Struct_sub [a P] : Π
(sub_Fst : τ a)
(sub_Snd : π (P sub_Fst) ), @τsub_ a P;
notation τsub_ quantifier;
constant symbol sub_ [a : Set] (P : τ a → Prop) : Set; notation sub_ quantifier;
rule τ (sub_ $P) ↪ τsub_ $P;
injective symbol sub_Fst [a P] (s : @τsub_ a P) : τ a;
rule sub_Fst (Struct_sub $1 $2) ↪ $1;
injective symbol sub_Snd [a P] (s : @τsub_ a P) : π (P (sub_Fst s)) ;
rule sub_Snd (Struct_sub $1 $2) ↪ $2;

// symbol foldl [b] [a] (f : τ b → τ a →  τ b) (i : τ b) : 𝕃 a → τ b;
// rule foldl $f $i □  ↪ $i
// with foldl $f $i ($x ⸬ $l) ↪ $f (foldl $f $i $l) $x ;

(4) The inductive command for now only generates the ind_ , ind_ℕ , ind𝕃, ... propositional-induction scheme for predicates in Prop; it should not be difficult to also generate rec , rec_ℕ , rec_𝕃 Set-recursion schemes for dependent types in Set? What is the motivation behind this absence ?

(5) The notations in the lambdapi-logics is inconsistent with the notation in lambdapi-stdlib (for example the use of τ versus El, the use of π versus Prf), AND ALSO inconsistent with the notation in the documentation or actual opam delivery code (for example list append in opam delivery is ⋅ \cdot versus ++ in the webpage https://github.com/Deducteam/lambdapi-stdlib/blob/master/List.lp). These silly issues could nevertheless waste an unfamiliar beginner's afternoon.

(6) The remove tactic in documentation https://lambdapi.readthedocs.io/en/latest/tactics.html#remove is absent from the actual opam delivery, and is not even a highlighted keyword by vscode.

(7) the have tactic should have a modifier so that it remains transparent instead of opaque DURING THE PROOF, for obvious reasons. Anyway, after the proof, the final proofterm will already transparently copy-replace all occurences of the variable introduced by have. My temporary solution is simply to copy-paste the (big) have term during the proof after tagging it with the identity function so it can be found quickly withing in the bigger proofterm:

(8) Last and most importantly, it is not clear where to find and how to use the translated Coq standard library inside the Lambdapi (here? https://github.com/Deducteam/lambdapi/tree/37c1730f243a1d9375e895eedafbdbe50542b4e5/out ). Would it be convenient to include it by default in the Lambdapi standard distribution? (it should be just a few MB data size?) A new tool such as Lambdapi would benefit from this usability even if it would be bad software engineering practice.

injective symbol DEBUG_TAG1 [a : Set] : τ a → τ a; rule DEBUG_TAG1 $x ↪ $x;

symbol T : Set;
symbol P : τ T → Set;

symbol test_have_opaque : Π t : τ T, Π p : τ (P t), τ `Σ_ t, P t ≔
begin
    assume t p;
    have t' : τ T //OPAQUE. NEED OPTION "@" FOR TRANSPARENT
    {
        refine (DEBUG_TAG1 t);
    };
    proofterm;
    //λ t p, ?23271.[t;p;DEBUG_TAG1 t]
    refine Struct_sigma t' p;

    //UNIFICATIO SUBGOAL GENERATED:
    // --------------------------------------------------------------------------------
    // 0. P t ≡ P t'
end; //ERROR: The proof is not finished:

(X) Did you know that Lambdapi is already doing computational category theory? In fact, Lambdapi's Set is made of the discrete concrete categories, and Set already have its own internal Π-types as defined in Deducteam/lambdapi-logics/U /DepArrow.lp. Therefore, the development of computational category theory within Lambdapi is well within the scope of receiving official Lambdapi dev support, financing, etc... I have an upcoming update:

Inductive datatypes or computation of concrete data limits via the abstract prover grammar: https://github.com/1337777/cartier/blob/master/cartierSolution14.lp https://github.com/1337777/cartier/blob/master/Kosta_Dosen_outline_alt.docx

example: the limit/equalizer of a (inductive) diagram when the (inductive-hypothesis) product cone [12;11]×[22;21]×[33;32;31] now is given an extra constant arrow [22;21] → [33;32;31] onto 31, besides its old discrete base diagram. The output is the limit cone apex object and side arrows and its universality:

// limit cone apex object
compute obj_category_Obj ((category_Obj_obj One) ∘>o (sigma_Fst (construct_inductively_limit_instance_liset _ example_graph_isf example_diagram)));
// (0,13,21,31) :: (0,13,22,31) :: (0,12,21,31) :: (0,12,22,31) :: (0,11,21,31) :: (0,11,22,31) :: nil

//limit cone sides arrows
compute arr_category_Arr ((Eval_cov_hom_transf ((sigma_Snd (construct_inductively_limit_instance_liset _ example_graph_isf example_diagram))₁ ))  ∘a' ( (@weightprof_Arr_arr _ _ _ (category_Obj_obj One) (graph_Obj_obj (Some (Some None))) One))  );
// λ x, natUniv_snd (natUniv_fst (natUniv_fst x))

//limit cone universality
compute arr_category_Arr (((((sigma_Snd (construct_inductively_limit_instance_liset _ example_graph_isf example_diagram))₂ ) _ _ _ example_cone) ∘>'_ ( _ ) ) ∘a' (Id_cov_arr (category_Obj_obj One))) liset_terminal_natUniv;
// Pair_natUniv (Pair_natUniv (Pair_natUniv (Base_natUniv 0) (Base_natUniv 12)) (Base_natUniv 22)) (Base_natUniv 31)

Did you already receive the help required in your job posting? Or have Deducteam given up on always being two steps ahead of trends in innovative algebra/logic-interoperable proof assistants?