Reimplement conversion modulo AC

[fblanqui]

This PR reimplements conversion modulo AC without enforcing terms to be in AC-canonical form.
This is much more efficient but may not work with any rewrite system (fix #1200).
It seems to work well with:

• the theory ACI = AC + Idempotence used in max-suc algebra for universe levels,
• the theory of commutative groups AG = AC + Inverse + Neutral used in linear arithmetic.

CHANGES:

• main changes are in term.ml and eval.ml
• Logger.set_debug_in: use string argument instead of char + permute arguments
• Print: rename without_qualifying into no_qualif
• List: add rev_append2
• Term: add type side = Left | Right, used in properties and rewrite tactic
• Term: remove property Assoc
• when declaring a symbol as associative commutative, a side must be given now

TODO:

• do not declare term as private and remove functions mk_
• handle commutativity alone, fix tests/OK/ac.lp
• fix compute
• in applications, compare arguments from left to right
• try improve eq_modulo further
• update CHANGES
• update doc, add links to examples
• Logger.set_debug: permute arguments?

[fblanqui]

@NotBad4U Could you please try this PR on some other examples for linear arithmetic ?

[fblanqui]

Be careful that I changed the ordering: arguments are now compared from left to right. So, you need to permute the arguments of var.

[NotBad4U]

I experimented the new AC on my previous test here. It is very fast now! Before we could only compute AC with ~20 variables, and I remember it took >5min for 23 variables. In the test, I can compute with 40 variables very quickly. I will try this feature on an SMT solver bench.

[NotBad4U]

@fblanqui I tried the new AC on my benchmarks and it is swift. I can do a computation with 500 variables, and it is faster than my current solution that compute the normal form without AC and reduces a term with a context varmap for none-interpreted term. In my current solution, the normalisation is fast but the calculation is very slow on large expression.
In my opinion, it is the multiple access to the context varmap that slow down the calculation. I still need to do more tests.

However, I have a strange behavior that I can even replicate in my gist. If I compute with only the ⇧ (reify function) then the term is reduced into cst 0.

compute (⇧ 
    (
        (T1 + T2 + T3)
        + (
            (— 1) * (T1 + T2  + T3)
        )
    )
);

However, if compose ⇧ with the interpretation function ⇓ such as:

compute ⇓ (⇧ 
    (
        (T1 + T2 + T3)
        + (
            (— 1) * (T1 + T2  + T3)
        )
    )
);

Then I got the result ((1 * T1) + ((1 * T2) + (1 * T3))) + ((-1 * T1) + ((-1 * T2) + (-1 * T3))). It looks like the ⇧ has not been applied. Do you have an idea why?

I updated the gist and the calculation is L127 if you want to reproduce on your side. Maybe we can add this gist in the folder /test/OK.

[NotBad4U]

It also does not work with my proof by reflexivity on reordering the pivot.
In the code below, the algebra that represents Clause does not compute an AC form.
The constructor P has an arity of 1. Does this PR normalize only symbols with an arity of 2?

symbol ℂ: TYPE;
symbol P: Prop → ℂ;
right associative commutative symbol ⊔: ℂ → ℂ → ℂ; notation ⊔ infix right 2;
symbol ⬓: ℂ;

symbol F: Clause → ℂ;

rule F ($x ⟇ $xs) ↪ (P $x) ⊔ (F $xs)
with F ▩ ↪ ⬓
;

sequential symbol  ⩦: ℂ → ℂ → 𝔹; notation ⩦ infix 11;
rule (P $x) ⩦ (P $x) ↪ true
with (P $x) ⩦ (P $y) ↪ false
with ($x ⊔ $xs) ⩦ ($y ⊔ $ys) ↪ ($x ⩦ $y) Stdlib.Bool.and ($xs ⩦ $ys)
with ⬓ ⩦ ⬓ ↪ true
with ⬓ ⩦ (P _) ↪ false
with (P _) ⩦ ⬓ ↪ false
with (_ ⊔ _) ⩦ ⬓ ↪ false
with ⬓ ⩦ (_ ⊔ _) ↪ false
with (P _) ⩦ (_ ⊔ _) ↪ false
with (_ ⊔ _) ⩦ (P _) ↪ false;

compute ((P b ⊔ P a ⊔ ⬓)  ⩦  (P a ⊔ P b ⊔ ⬓)); // No AC computed here