Bug with set ?

lia.lp

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.HOL;
require open Stdlib.Eq;
require open Stdlib.Set;
require open Stdlib.Z;
require open Stdlib.Pos;
require open Stdlib.Bool;
require open Stdlib.Comp;
require open Stdlib.Impred;

constant symbol Ring : TYPE;
symbol ring : Set;
rule τ ring ↪ Ring;

associative commutative symbol ⨦ : Ring → Ring → Ring; notation ⨦ infix left 20;
symbol Mul : ℤ → Ring → Ring; // multiplication
constant symbol Z : Ring;

injective symbol C: ℤ → Ring; // constant

injective symbol Var: ℤ → Ring;

// Add this rule to Stdlib?
rule ~ ~ $x ↪ $x;

// Reify function from ℤ to Ring
sequential symbol ⇧ : ℤ → Ring; notation ⇧ prefix 10;

rule ⇧ $x + $y ↪ (⇧ $x) ⨦ (⇧ $y)
with ⇧ (Zpos $x) × $y ↪ Mul (Zpos $x) (⇧ $y)
with ⇧  $y × (Zpos $x) ↪ Mul (Zpos $x) (⇧ $y)
with ⇧ (Zneg $x) × $y ↪ Mul (Zneg $x) (⇧ $y)
with ⇧  $y × (Zneg $x) ↪ Mul (Zpos $x) (⇧ $y)
with ⇧ (Zpos $x) ↪ C (Zpos $x)
with ⇧ (Zneg $x) ↪ C (Zneg $x)
with ⇧ 0 ↪ Z
with ⇧ (~ $var) ↪ Mul (Zneg H) (Var $var)
with ⇧ $var ↪ Mul 1 (Var $var)
;


// Rewriting system for Ring
rule Z ⨦ $x ↪ $x
with $x ⨦ Z ↪ $x

with Mul $a (Mul $b $x) ↪ Mul ($a × $b) $x
with Mul $a ($x ⨦ $y) ↪ (Mul $a $x) ⨦ (Mul $a $y)

with (C $x) ⨦ (C $y) ↪ C ($x + $y)
with (C $x) ⨦ ((C $y) ⨦ $z) ↪ C ($x + $y) ⨦ $z
with (Mul $k $x) ⨦ (Mul $l $x) ↪ Mul ($k + $l) $x
with (Mul $k $x) ⨦ ((Mul $l $x) ⨦ $y) ↪ (Mul ($k + $l) $x) ⨦ $y

with C 0 ↪ Z
with Mul 0 _ ↪ Z
with Mul 1 (C $x) ↪ (C $x) // necessary ?
with Mul $x (C $y) ↪ C ($x × $y) // necessary ?
;

// Decidable comparaison between Ring
symbol ≥? : τ ring → τ ring → 𝔹; notation ≥? infix 10;

rule C $x ≥? C $y ↪ isGt ($x ≐ $y) Stdlib.Bool.or (isEq ($x ≐ $y))
with Z ≥? Z ↪ true
with Z ≥? C (Zpos _) ↪ false
with C (Zpos _) ≥? Z ↪ true
with Z ≥? C (Zneg _) ↪ true
with C (Zneg _) ≥? Z ↪ false
with (Mul $k $x) ≥? (Mul $l $x) ↪ isGt ($k ≐ $l) Stdlib.Bool.or (isEq ($k ≐ $l))
;

symbol correctness_lia a b: π (istrue ((⇧ a) ≥? ⇧ b)) → π (a ≥ b);

symbol completude_lia a b: π (a ≥ b) → π (istrue ((⇧ a) ≥? ⇧ b));

symbol f : τ (int ⤳ int);

symbol p_2 ≔ ((f 5) ≤ 4);

symbol p_3 ≔ (f 5);


symbol test_lia:  π ((¬ (p_3 < 5)) ∨ p_2) ≔
begin
set H0l ≔ (f 5);
set H0r ≔ 5;
set H1l ≔ (f 5);
set H1r ≔ 4;
have Hla : π (¬ (H0l < H0r) ∨ (H1l ≤ H1r)) {
    // ... applying the Farkas coefficient [1,1] and transform inequalities to sum them and derive a contradiction
    set H0l' ≔ (1 × ((~ H0l) - (~ H0r)));
    set H0r' ≔ (1 × (0 + 1));
    set H1l' ≔ (1 × (H1l - H1r));
    set H1r' ≔ (1 × (0 + 1));
    have Hsum : π (H0l' + H1l' ≥ H0r' + H1r') { // Equation (1)
        admit
    };
    // ==== END DEFINE THE ALETHE ALGO ==============
    compute ⇧ (H0l' + H1l');
    compute (C (Zpos H) ⨦ (Mul (Zneg H) (Var (f (Zpos (I (O H))))) ⨦ Mul (Zpos H) (Var (f (Zpos (I (O H))))))); // result of the previous compute paste here -- but it is reduce here if we compute again.
    compute ⇧ (H0r' + H1r');
    apply completude_lia (H0l' + H1l') (H0r' + H1r') Hsum; //FIXME: it sounds to not work...
};
// ...
end;


// Same computation than Equation (1) but without using `set X ≔`
symbol test_lia2:  π (
    (1 × ((~ (f 5)) - (~ 5))) + (1 × ((f 5) - 4))
    ≥
    (1 × (0 + 1)) + (1 × (0 + 1))
) ≔
begin
refine correctness_lia ((1 × ((~ (f 5)) - (~ 5))) + (1 × ((f 5) - 4))) ((1 × (0 + 1)) + (1 × (0 + 1))) _;
simplify // Here it reduces correctly to \bot
end;