Rewriting rules do not compute correctly on term defined by a `set` tactic ?

[NotBad4U]

Hi everyone,

I am facing a strange behavior that I tried to summarize in this gist. I am using the set tactic in my generated proof to make the reconstruction of linear arithmetic proof more readable/easier to debug.

A linear inequality is a term of the form:

∑_i 𝑐𝑖 × 𝑡𝑖 + 𝑑1 ⋈ ∑_i 𝑐𝑖 × 𝑡𝑖 + 𝑑2

With ⋈ \in {=, <, >, ≤, ≥}. I am using the tactic set to abstract the left and right terms of an inequality. For example set His := 𝑐𝑖 × 𝑡𝑖 + 𝑑1 and set Hir := 𝑐𝑖 × 𝑡𝑖 + 𝑑2.

It makes the generation of the proof easier and more compact because Alethe requires some normalization before having the sum of the resulting literals, which is trivially contradictory.

∑_k ∑_i 𝑐 𝑘𝑖 ∗ 𝑡𝑘𝑖 ⋈ ∑_k 𝑑𝑘

My problem is that if I use set in a proof then the computation do not work correctly (check line 103). If I try to compute manually with compute each part of the final inequality, it produces a term that is not a constant but if I take the output from the terminal and compute again then it reduce to a constant. But if I do not use set then we can see that it compute line 117.

[fblanqui]

A first remark: the rule at line 39 catches everything and will probably be applied all the time. This is not what you expect I guess. It is an example where it might be useful to declare a symbol sequential, but this may break important properties. This kind of reification should be internalized using builtins to avoid adding this kind of rules in the conversion.

[fblanqui]

Other remarks:

• the rule line 51 is an extension of the rule line 50 to take car of contexts: you probably need similar extensions for other rules like the ones on line 44, 45, 52, 53
• line 64: use a let to share the computation of $x ≐ $y
• rules line 64-70: there is no rule
• line 73-74: correctness/completeness. I am not sure that this is what you really want (see below). It should be easy to prove anyway since, by induction, a and b are only of the form Z0, Zpos or Zneg.

Following the implementation of reflexive tactics, don't you want instead:

• define an interpretation function I from Ring to Z given a valuation of variables in Z
• define a function nf from Ring to Ring that computes the normal form of a Ring expression
• prove that nf is correct, that is, preserves the interpretation: forall v, I (nf t) v = I t v

Then, to prove that t:Z = u:Z you can proceed as follows:

• externally compute t', u' and v such that I t' v ≡ t and I u' v ≡ u (reification)
• apply correctness of nf to get as goal I (nf t') v = I (nf u') v
• conclude by reflexivity

[fblanqui]

Proposal:

require open Stdlib.Z;

constant symbol R : TYPE;

symbol var : ℤ → ℤ → R;
/* semantics: [var k x] = k * x
note that the second argument could be any type that has a ring structure
(we then would take R : TYPE → TYPE) */
constant symbol cst:ℤ → R;
symbol opp:R → R;
right associative commutative symbol add:R → R → R;

rule var 0 _ ↪ cst 0;

rule opp (var $k $x) ↪ var (~ $k) $x
with opp (cst $k) ↪ cst (~ $k)
with opp (opp $x) ↪ $x
with opp (add $x $y) ↪ add (opp $x) (opp $y);
// note that opp is totally defined on terms built with var, cst, opp and add, i.e. no normal form contains opp

rule add (var $k $x) (var $l $x) ↪ var ($k + $l) $x
with add (var $k $x) (add (var $l $x) $y) ↪ add (var ($k + $l) $x) $y
with add (cst $k) (cst $l) ↪ cst ($k + $l)
with add (cst $k) (add (cst $l) $y) ↪ add (cst ($k + $l)) $y
with add (cst 0) $x ↪ $x
with add $x (cst 0) ↪ $x;

// example:
compute λ x y z, add (add (var 1 x) (add (opp (var 1 y)) (var 1 z))) (add (var 1 y) (var 1 x));

// multiplication by a constant (optional)
symbol mul:ℤ → R → R;
rule mul $k (var $l $z) ↪ var ($k × $l) $z
with mul $k (opp $r) ↪ mul (~ $k) $r
with mul $k (add $r $s) ↪ add (mul $k $r) (mul $k $s)
with mul $k (cst $z) ↪ cst ($k × $z)
with mul $k (mul $l $z) ↪ mul ($k × $l) $z;
// note that mul is totally defined on terms built from var, cst, opp, add and mul, i.e. no normal form contains mul

// reification
// WARNING: this symbol is declared as sequential
// and the reduction relation is not stable by substitution
sequential symbol ⇧ : ℤ → R;

rule ⇧ 0 ↪ cst 0
with ⇧ (Zpos $x) ↪ cst (Zpos $x)
with ⇧ (Zneg $x) ↪ cst (Zneg $x)
with ⇧ (~ $x) ↪ opp (⇧ $x)
with ⇧ ($x + $y) ↪ add (⇧ $x) (⇧ $y)

with ⇧ (0 × $y) ↪ mul 0 (⇧ $y)
with ⇧ (Zpos $x × $y) ↪ mul (Zpos $x) (⇧ $y)
with ⇧ (Zneg $x × $y) ↪ mul (Zneg $x) (⇧ $y)
with ⇧ ($y × 0) ↪ mul 0 (⇧ $y)
with ⇧ ($y × Zpos $x) ↪ mul (Zpos $x) (⇧ $y)
with ⇧ ($y × Zneg $x) ↪ mul (Zneg $x) (⇧ $y)

with ⇧ $x ↪ var 1 $x; // must be the last rule for ⇧

// example:
compute λ x y z, ⇧ ((x + ((~ y) + z)) + (y + x));

[NotBad4U]

Do we agree on the correctness lemmas?

// eval function
symbol ⇓: R → ℤ;
rule ⇓ (var $k $x) ↪ $k × $x
with ⇓ (cst $k) ↪ $k
with ⇓ (opp $x) ↪ ~ (⇓ $x)
with ⇓ (add $x $y) ↪ ⇓ $x + ⇓ $y
;

sequential symbol norm: R → R;
rule norm (add $x (cst 0)) ↪ $x
with norm (add $x (opp $x)) ↪ cst 0
with norm (opp (cst 0)) ↪ cst 0
with norm (opp (opp $x)) ↪ $x
with norm (opp (add $x $y)) ↪ add (opp $x) (opp $y)
with norm $x ↪ $x
;

symbol eqz : ℤ → ℤ → 𝔹;
rule eqz (Zpos $x) (Zpos $y) ↪ isEq (compare $x $y)
with eqz (Zneg $x) (Zneg $y) ↪ isEq (compare $x $y)
with eqz Z0 Z0 ↪ true
with eqz (Zpos _) (Zneg _) ↪ false
with eqz (Zneg _) (Zpos _) ↪ false
;

sequential symbol =R : R → R → 𝔹; notation =R infix 10;
// var
rule var $k $x =R var $l $x ↪ eqz $k $l
with var $k $x =R var $l $y ↪ false
with var $k $x =R _ ↪ false
with cst $x =R cst $y ↪ eqz $x $y
with cst $x =R _ ↪ false
// opp
with opp $x =R opp $y ↪ $x =R $y
with opp _ =R cst _ ↪ false
// add 
with add $x $y =R  add $u $v ↪ ($x =R $u) and ($y =R $v)
with add _ _ =R _ ↪ false
;

// Correctness of the normalization function
symbol norm_correct (r: R) : π ((⇓ r) =  ⇓ (norm r));

// Correctness of our decision procedure
symbol f_correct : Π (r1 r2: R), π ((norm r1 =R norm r2) = true) → π (⇓ r1 = ⇓ r2);

rule (Zpos H) × $x ↪ $x;

assert x ⊢ 1 × x ≡ x;


symbol test x y : π (x + y + 0 = y + x + 0) ≔
begin
assume x y;
have H: π ((⇓ (⇧(x + y + 0))) = ⇓ (⇧ (y + x + 0))) → π (x + y + 0 = y + x + 0) {
    assume H;
    //refine H;  // STUCK
    admit
};
refine H _;
refine f_correct (⇧ _) (⇧ _) _;
apply eq_refl
end;

But I do not see how we can apply H:

have H: π ((⇓ (⇧(x + y + 0))) = ⇓ (⇧ (y + x + 0))) → π (x + y + 0 = y + x + 0) {
 assume H; refine H;
}

because the evaluation (⇓) will not evaluate to the same terms (x and y are swap because of AC).

[fblanqui]

Do you really want/need to prove the correctness and completeness inside Lambdapi? To do that, you need to have a formalization of what Lambdapi is doing. A pen-and-paper proof outside Lambdapi seems more reasonable to start with.

[NotBad4U]

I am not sure to follow you. Do you mean putting this lemma as an axiom? symbol f_correct : Π (r1 r2: R), π ((norm r1 =R norm r2) = true) → π (⇓ r1 = ⇓ r2);

To do that, you need to have a formalization of what Lambdapi is doing.

This is necessary to prove the reify part?

[fblanqui]

Let's try to describe what we are trying to do:

1. We assume given two Lambdapi terms u and v of type Z, and we want to prove that they are propositionally equal, that is, the goal to prove is t=u.
2. For all Lambdapi terms t, we have ⇓(⇧t) ≡ t. This can be proved by induction on the structure of t, right?
3. Hence, (t=u) ≡ (⇓(⇧t) = ⇓(⇧u)) and we can instead try to prove ⇓(⇧t) = ⇓(⇧u).
4. Consider now the inductive type R' generated by var, cst, opp and add (R is a quotient of R'), and let =R be the smallest equivalence relation on R' stable by substitution and context containing the equations saying that (R',add,cst 0,opp) is a commutative group (R is isomorphic to R'/=R).
5. We could first prove that, for all terms r,s:R', if r =R s, then ⇓r = ⇓s, by induction on =R, using the fact that (Z,+,0,~) is a commutative group.
6. We could then prove that the properties (add is AC) and rules of var, opp and add, ensure that r =R s if r ≡ s, that is, that the normal forms and r and s computed by Lambdapi are syntactically equal. This is the key point.
7. Hence, ⇓(⇧t) = ⇓(⇧u) can eventually be proved by reflexivity because ⇓(⇧t) = ⇓(⇧u) if⇧t =R ⇧u if ⇧t ≡ ⇧u.

The items 4) and 5) could be formalized in Lambdapi itself easily as it is a property of R', =R and Z.

The item 3) is about Lambdapi terms themselves. It is possible to formalize it in Lambdapi itself but it is not very interesting.

You can get 6) by proving the correctness of the evaluation process of Lambdapi in this context, that is, using the declared properties and rules of var, opp and add. If we write nf(t) the normal form computed by Lambdapi of the term t, it is enough to prove its correctness wrt =R, that is, nf(r) =R r, for all terms r:R. This should not be too difficult to prove when you know how nf is implemented, and could probably be formalized in Lambdapi itself, though not within a few lines.

Note that we do not need nf to be complete although it is a desirable property. Completeness means that any two terms equivalent in the theory =R have the same normal form: r =T s => nf(r) = nf(s). This is more difficult to prove.

[NotBad4U]

Thanks for this exhaustive description.

I think step 2) has a problem because ⇓(⇧t) ≡ t. is incorrect because of AC. Consider the term y + x, which is then reified into add (mul 1 x) (mul 1 y), and then evaluated back into x + y. So, we do not have ⇓(⇧t) ≡ t if we use AC. We can prove that for any t: Z then ⇓(⇧t) = t,, but it can be proved only for the constructor of Z i.e. Zpos, Zneg, Z.

[fblanqui]

Right, but we have ⇓(⇧t) = t, don't we? And it is enough, no?

[NotBad4U]

If t is a term of type Z, then I think we can easily prove that for all t: Z, ⇓(⇧t) = t by induction on t.

[fblanqui]

And do you agree with 5 and 6?

[fblanqui]

Concerning 6, following https://doi.org/10.4230/LIPIcs.FSCD.2022.24, you have that nf(t) is the normal form of the AC-canonical form of t wrt the rewrite relation -->_R^AC which consists in alternating rewriting wrt the set R of rewrite rules given above for var, opp and add using syntactic matching, and AC canonization which consists in normalizing wrt to the following rules:

• add (add x y) z --> add x (add y z) [right associativity]
• add x y --> add y x if x > y
• add x (add y z) --> add y (add x z) if x > y

where > is a total ordering such that (var k x) < (var l y) iff x < y or else x = y and k < l, and similarly for the other function symbols (the arguments of function applications are compared from right to left).

[fblanqui]

Hi. I propose to close this issue as well because the initial problem is not clear at all, and the following discussion is not related actually.