lia-without-ac

gistfile1.txt

require open Stdlib.Nat Stdlib.Z Stdlib.Set Stdlib.Prop Stdlib.Bool Stdlib.Comp Stdlib.List;

constant symbol R : TYPE;

constant symbol cst:ℤ → R;

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) */
symbol opp:R → R;
symbol add:R → R → R;

symbol mif : 𝔹 → R → R → R;

rule mif true  $x _ ↪ $x
with mif false _ $y ↪ $y;

symbol addnorm: R → R → R;

// norm
rule addnorm (var $k $i) (var $l $j) ↪ mif ($i Stdlib.Nat.≤ $j)
                                        (add (var $k $i) (var $l $j))
                                        (add (var $l $j) (var $k $i))

with addnorm (add (var $c1 $i) $xs) (add (var $c2 $j) $ys) ↪
    mif ($i Stdlib.Nat.≤ $j)
        (add (var $c1 $i) (addnorm $xs (add (var $c2 $j) $ys)))
    // else
        (add (var $c2 $j) (addnorm (add (var $c1 $i) $xs) $ys))

with addnorm (add (var $c1 $i) $xs) (var $c2 $j) ↪
    mif ($i Stdlib.Nat.≤ $j)
    (add (var $c1 $i) (addnorm $xs (var $c2 $j)))
    // else
    (add (var $c2 $j) (addnorm (var $c1 $i) $xs))

with addnorm (var $c1 $i) (add (var $c2 $j) $ys) ↪
    mif ($i Stdlib.Nat.≤ $j)
        (add (var $c1 $i) (addnorm (var $c2 $j) $ys))
    // else
        (add (var $c2 $j) (addnorm (var $c1 $i) $ys))

with addnorm (cst $c1) (cst $c2) ↪  (cst ($c1 + $c2))
with addnorm (cst $c) (var $k $i) ↪  add (cst $c) (var $k $i)
with addnorm (var $k $i) (cst $c) ↪  add (cst $c) (var $k $i)
with addnorm (add (cst $x) $xs) (add (cst $a) $ys) ↪ add (cst ($x + $a)) (addnorm $xs $ys)
with addnorm (cst $x) (add (cst $a) $tl) ↪ addnorm (cst ($x + $a)) $tl
with addnorm (add $x $xs) (cst $c) ↪ add (cst $c) (addnorm $x $xs)

with addnorm (add (var $k $i) $xs) (add (cst $c) $ys) ↪
    (add (cst $c) (addnorm (add (var $k $i) $xs) $ys))
with addnorm (add (cst $c) $xs) (add (var $k $i) $ys) ↪
    (add (cst $c) (addnorm $xs (add (var $k $i) $ys)))
with addnorm (add (cst $c1) $y) (add (cst $c2) $b) ↪
    (add (cst ($c1 + $c2)) (addnorm $y $b))                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 


with addnorm (var $c1 $i) (add (var $c2 $j) $tl) ↪
    mif ($i Stdlib.Nat.≤ $j)
        (add (var $c1 $i) (addnorm (var $c2 $j) $tl))
        (add (var $c2 $j) (addnorm (var $c1 $i) $tl))
;


compute (addnorm (addnorm (var _1 Stdlib.Nat._4)
(addnorm (var _1 Stdlib.Nat._3) (addnorm  (addnorm (var _1 Stdlib.Nat._5) (var _1 Stdlib.Nat._2)) (addnorm (var _1 Stdlib.Nat._1) (var _1 Stdlib.Nat._0)))))
    (addnorm (var _1 Stdlib.Nat._3) (addnorm (var _1 Stdlib.Nat._2) (addnorm (var _1 Stdlib.Nat._1) (var _1 Stdlib.Nat._0)))));

compute (addnorm (addnorm (var _1 Stdlib.Nat._5) (var _1 Stdlib.Nat._2)) (var _1 Stdlib.Nat._1) );

// print eqn;

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 $c1 $i) (var $c2 $i) ↪ (var ($c1 + $c2) $i)
with add (var $c1 $i) (add (var $c2 $i) $y) ↪ (add (var ($c1 + $c2) $i) $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
;

print 𝕃;

symbol T1: τ int;
symbol T2: τ int;
symbol T3: τ int;
symbol T4: τ int;
symbol T5: τ int;

symbol env ≔ T1 ⸬ T2 ⸬ T3 ⸬ T4 ⸬ □;

print env;

// 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 $i) ↪ var ($k * $l) $i
with mul $k (opp $r) ↪ mul (— $k) $r
with mul $k (add $x $y) ↪ add (mul $k $x) (mul $k $y)
with mul $k (cst $c) ↪ cst ($k * $c)
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 get_env' : 𝕃 int → ℤ → 𝕃 int;
rule get_env' $l (Zpos _) ↪ $l
with get_env' $l (Zneg _) ↪ $l
with get_env' $l Z0 ↪ $l
with get_env' $l ($x + $y) ↪ (get_env' $l $x) ++ (get_env' $l $y)
with get_env' $l ($x * $y) ↪ (get_env' $l $x) ++ (get_env' $l $y)
with get_env' $l (— $x) ↪ get_env' $l $x
with get_env' $l $x ↪ $x ⸬ $l
;

symbol get_env : ℤ → 𝕃 int ≔  λ (f: ℤ), get_env' □ f;


sequential symbol eqℤ: τ int → τ int → 𝔹;
rule eqℤ $x $x ↪ true
with eqℤ $x $y ↪ false;

sequential symbol reify : 𝕃 int →  ℤ → R;
rule reify $env 0 ↪ cst 0
with reify $env (Zpos $x) ↪ cst (Zpos $x)
with reify $env (Zneg $x) ↪ cst (Zneg $x)
with reify $env (— $x) ↪ opp (reify $env $x)
with reify $env ($x + $y) ↪ addnorm (reify $env $x) (reify $env $y)

with reify $env (0 * $y) ↪ mul 0 (reify $env $y)
with reify $env (Zpos $x * $y) ↪ mul (Zpos $x) (reify $env $y)
with reify $env (Zneg $x * $y) ↪ mul (Zneg $x) (reify $env $y)
with reify $env ($y * 0) ↪ mul 0 (reify $env $y)
with reify $env ($y * Zpos $x) ↪ mul (Zpos $x) (reify $env $y)
with reify $env ($y * Zneg $x) ↪ mul (Zneg $x) (reify $env $y)

with reify $env $x ↪ var 1 (index (eqℤ) $x $env); // must be the last rule for reify


symbol f ≔ T1 + (_7 * T2) + T2 + T1;

symbol σ ≔ get_env f;

compute (reify (get_env f) f);

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

symbol not_found: τ int;

// eval function
symbol eval: 𝕃 int → R → ℤ;
rule eval $env (var $k $i) ↪ $k * (nth not_found $env $i)
with eval _ (cst $k) ↪ $k
with eval $env (opp $x) ↪ — (eval $env $x)
with eval $env (add $x $y) ↪ (eval $env $x) + (eval $env $y)
;

symbol T6: τ int;
symbol T7: τ int;
symbol T8: τ int;
symbol T9: τ int;
symbol T10: τ int;
symbol T11: τ int;
symbol T12: τ int;
symbol T13: τ int;
symbol T14: τ int;
symbol T15: τ int;
symbol T16: τ int;
symbol T17: τ int;
symbol T18: τ int;
symbol T19: τ int;
symbol T20: τ int;
symbol T21: τ int;
symbol T22: τ int;
symbol T23: τ int;
symbol T24: τ int;
symbol T25: τ int;
symbol T26: τ int;
symbol T27: τ int;
symbol T28: τ int;
symbol T29: τ int;
symbol T30: τ int;
symbol T31: τ int;
symbol T32: τ int;
symbol T33: τ int;
symbol T34: τ int;
symbol T35: τ int;
symbol T36: τ int;
symbol T37: τ int;
symbol T38: τ int;
symbol T39: τ int;
symbol T40: τ int;

symbol f2 ≔ (
    (T1 + T2 + T3 + T4 + T5 + T6 + T7 + T8 + T9 + T10 + T11 + T12 + T13 + T14 + T15 + T16 + T17 + T18 + T19 + T20)
    + (
        (— 1) * (T20 + T19 + T18 + T17 + T16 + T15 + T14 + T13 + T12 + T11 + T10 + T9 + T8 + T7 + T6 + T5 + T4 + T3 + T2 + T1) + 0
    )
);
print f2;

compute eval (get_env f2) (reify (get_env f2) f2);

symbol p_0_0 : τ (int);
symbol p_0_1 : τ (int);
symbol p_0_2 : τ (int);
symbol p_0_3 : τ (int);
symbol p_0_4 : τ (int);
symbol p_0_5 : τ (int);
symbol p_1_0 : τ (int);
symbol p_1_1 : τ (int);
symbol p_1_2 : τ (int);
symbol p_1_3 : τ (int);
symbol p_1_4 : τ (int);
symbol p_1_5 : τ (int);
symbol p_2_0 : τ (int);
symbol p_2_1 : τ (int);
symbol p_2_2 : τ (int);
symbol p_2_3 : τ (int);
symbol p_2_4 : τ (int);
symbol p_2_5 : τ (int);
symbol p_3_0 : τ (int);
symbol p_3_1 : τ (int);
symbol p_3_2 : τ (int);
symbol p_3_3 : τ (int);
symbol p_3_4 : τ (int);
symbol p_3_5 : τ (int);
symbol p_4_0 : τ (int);
symbol p_4_1 : τ (int);
symbol p_4_2 : τ (int);
symbol p_4_3 : τ (int);
symbol p_4_4 : τ (int);
symbol p_4_5 : τ (int);
symbol p_5_0 : τ (int);
symbol p_5_1 : τ (int);
symbol p_5_2 : τ (int);
symbol p_5_3 : τ (int);
symbol p_5_4 : τ (int);
symbol p_5_5 : τ (int);
symbol p_6_0 : τ (int);
symbol p_6_1 : τ (int);
symbol p_6_2 : τ (int);
symbol p_6_3 : τ (int);
symbol p_6_4 : τ (int);
symbol p_6_5 : τ (int);

// //notation + infix left 20;

symbol H0l' ≔  (1 * ((— (p_0_4 + p_1_4 + p_2_4 + p_3_4 + p_4_4 + p_5_4)) - (— 1)));
symbol H1l' ≔ (1 * ((— (p_0_1 + p_1_1 + p_2_1 + p_3_1 + p_4_1 + p_5_1)) - (— 1)));

symbol sum ≔ H0l' + H1l';

symbol Env ≔ (get_env sum);

compute (reify Env sum);

symbol pidgeon5: π ⊤ ≔
begin
set H0l' ≔ (1 * ((— (p_0_4 + p_1_4 + p_2_4 + p_3_4 + p_4_4 + p_5_4)) - (— 1)));
set H0r' ≔ (1 * 0);
set H1l' ≔ (1 * ((— (p_0_1 + p_1_1 + p_2_1 + p_3_1 + p_4_1 + p_5_1)) - (— 1)));
set H1r' ≔ (1 * 0);
set H2l' ≔ (1 * ((— (— 1 * (p_5_0 + p_5_1 + p_5_2 + p_5_3 + p_5_4))) - (— (— 1 * 1))));
set H2r' ≔ (1 * 0);
set H3l' ≔ (1 * ((— (— 1 * (p_4_0 + p_4_1 + p_4_2 + p_4_3 + p_4_4))) - (— (— 1 * 1))));
set H3r' ≔ (1 * 0);
set H4l' ≔ (1 * ((— (— 1 * (p_3_0 + p_3_1 + p_3_2 + p_3_3 + p_3_4))) - (— (— 1 * 1))));
set H4r' ≔ (1 * 0);
set H5l' ≔ (1 * ((— (— 1 * (p_2_0 + p_2_1 + p_2_2 + p_2_3 + p_2_4))) - (— (— 1 * 1))));
set H5r' ≔ (1 * 0);
set H6l' ≔ (1 * ((— (— 1 * (p_1_0 + p_1_1 + p_1_2 + p_1_3 + p_1_4))) - (— (— 1 * 1))));
set H6r' ≔ (1 * 0);
set H7l' ≔ (1 * ((— (— 1 * (p_0_0 + p_0_1 + p_0_2 + p_0_3 + p_0_4))) - (— (— 1 * 1))));
set H7r' ≔ (1 * 0);
set H8l' ≔ (1 * ((— (p_0_0 + p_1_0 + p_2_0 + p_3_0 + p_4_0 + p_5_0)) - (— 1)));
set H8r' ≔ (1 * 0);
set H9l' ≔ (1 * ((— (p_0_2 + p_1_2 + p_2_2 + p_3_2 + p_4_2 + p_5_2)) - (— 1)));
set H9r' ≔ (1 * 0);
set H10l' ≔ (1 * ((— (p_0_3 + p_1_3 + p_2_3 + p_3_3 + p_4_3 + p_5_3)) - (— 2)));
set H10r' ≔ (1 * (0 + 1));
set H11l' ≔ (1 * (((p_0_4 + p_1_4 + p_2_4 + p_3_4 + p_4_4 + p_5_4) + (p_0_1 + p_1_1 + p_2_1 + p_3_1 + p_4_1 + p_5_1) + (— 1 * (p_5_0 + p_5_1 + p_5_2 + p_5_3 + p_5_4)) + (— 1 * (p_4_0 + p_4_1 + p_4_2 + p_4_3 + p_4_4)) + (— 1 * (p_3_0 + p_3_1 + p_3_2 + p_3_3 + p_3_4)) + (— 1 * (p_2_0 + p_2_1 + p_2_2 + p_2_3 + p_2_4)) + (— 1 * (p_1_0 + p_1_1 + p_1_2 + p_1_3 + p_1_4)) + (— 1 * (p_0_0 + p_0_1 + p_0_2 + p_0_3 + p_0_4)) + (p_0_0 + p_1_0 + p_2_0 + p_3_0 + p_4_0 + p_5_0) + (p_0_2 + p_1_2 + p_2_2 + p_3_2 + p_4_2 + p_5_2) + (p_0_3 + p_1_3 + p_2_3 + p_3_3 + p_4_3 + p_5_3)) - (1 + 1 + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + 1 + 1 + 2)));
set H11r' ≔ (1 * 0);
set σ ≔ get_env ((((((((((((H0l' + H1l') + H2l') + H3l') + H4l') + H5l') + H6l') + H7l') + H8l') + H9l') + H10l') + H11l'));
compute σ; 

compute (reify σ (((((((((((H0l' + H1l') + H2l') + H3l') + H4l') + H5l') + H6l') + H7l') + H8l') + H9l') + H10l') + H11l'));
apply ⊤ᵢ;
end;

// symbol pidgeon6: π ⊤ ≔
// begin
// set H0l' ≔ (1 * ((— (p_0_5 + p_1_5 + p_2_5 + p_3_5 + p_4_5 + p_5_5 + p_6_5)) - (— 1)));
// set H0r' ≔ (1 * 0);
// set H1l' ≔ (1 * ((— (p_0_2 + p_1_2 + p_2_2 + p_3_2 + p_4_2 + p_5_2 + p_6_2)) - (— 1)));
// set H1r' ≔ (1 * 0);
// set H2l' ≔ (1 * ((— (p_0_0 + p_1_0 + p_2_0 + p_3_0 + p_4_0 + p_5_0 + p_6_0)) - (— 1)));
// set H2r' ≔ (1 * 0);
// set H3l' ≔ (1 * ((— (— 1 * (p_0_0 + p_0_1 + p_0_2 + p_0_3 + p_0_4 + p_0_5))) - (— (— 1 * 1))));
// set H3r' ≔ (1 * 0);
// set H4l' ≔ (1 * ((— (— 1 * (p_1_0 + p_1_1 + p_1_2 + p_1_3 + p_1_4 + p_1_5))) - (— (— 1 * 1))));
// set H4r' ≔ (1 * 0);
// set H5l' ≔ (1 * ((— (— 1 * (p_2_0 + p_2_1 + p_2_2 + p_2_3 + p_2_4 + p_2_5))) - (— (— 1 * 1))));
// set H5r' ≔ (1 * 0);
// set H6l' ≔ (1 * ((— (— 1 * (p_3_0 + p_3_1 + p_3_2 + p_3_3 + p_3_4 + p_3_5))) - (— (— 1 * 1))));
// set H6r' ≔ (1 * 0);
// set H7l' ≔ (1 * ((— (— 1 * (p_4_0 + p_4_1 + p_4_2 + p_4_3 + p_4_4 + p_4_5))) - (— (— 1 * 1))));
// set H7r' ≔ (1 * 0);
// set H8l' ≔ (1 * ((— (— 1 * (p_5_0 + p_5_1 + p_5_2 + p_5_3 + p_5_4 + p_5_5))) - (— (— 1 * 1))));
// set H8r' ≔ (1 * 0);
// set H9l' ≔ (1 * ((— (— 1 * (p_6_0 + p_6_1 + p_6_2 + p_6_3 + p_6_4 + p_6_5))) - (— (— 1 * 1))));
// set H9r' ≔ (1 * 0);
// set H10l' ≔ (1 * ((— (p_0_1 + p_1_1 + p_2_1 + p_3_1 + p_4_1 + p_5_1 + p_6_1)) - (— 1)));
// set H10r' ≔ (1 * 0);
// set H11l' ≔ (1 * ((— (p_0_3 + p_1_3 + p_2_3 + p_3_3 + p_4_3 + p_5_3 + p_6_3)) - (— 1)));
// set H11r' ≔ (1 * 0);
// set H12l' ≔ (1 * ((— (p_0_4 + p_1_4 + p_2_4 + p_3_4 + p_4_4 + p_5_4 + p_6_4)) - (— 2)));
// set H12r' ≔ (1 * (0 + 1));
// set H13l' ≔ (1 * (((p_0_5 + p_1_5 + p_2_5 + p_3_5 + p_4_5 + p_5_5 + p_6_5) + (p_0_2 + p_1_2 + p_2_2 + p_3_2 + p_4_2 + p_5_2 + p_6_2) + (p_0_0 + p_1_0 + p_2_0 + p_3_0 + p_4_0 + p_5_0 + p_6_0) + (— 1 * (p_0_0 + p_0_1 + p_0_2 + p_0_3 + p_0_4 + p_0_5)) + (— 1 * (p_1_0 + p_1_1 + p_1_2 + p_1_3 + p_1_4 + p_1_5)) + (— 1 * (p_2_0 + p_2_1 + p_2_2 + p_2_3 + p_2_4 + p_2_5)) + (— 1 * (p_3_0 + p_3_1 + p_3_2 + p_3_3 + p_3_4 + p_3_5)) + (— 1 * (p_4_0 + p_4_1 + p_4_2 + p_4_3 + p_4_4 + p_4_5)) + (— 1 * (p_5_0 + p_5_1 + p_5_2 + p_5_3 + p_5_4 + p_5_5)) + (— 1 * (p_6_0 + p_6_1 + p_6_2 + p_6_3 + p_6_4 + p_6_5)) + (p_0_1 + p_1_1 + p_2_1 + p_3_1 + p_4_1 + p_5_1 + p_6_1) + (p_0_3 + p_1_3 + p_2_3 + p_3_3 + p_4_3 + p_5_3 + p_6_3) + (p_0_4 + p_1_4 + p_2_4 + p_3_4 + p_4_4 + p_5_4 + p_6_4)) - (1 + 1 + 1 + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + (— 1 * 1) + 1 + 1 + 2)));
// set H13r' ≔ (1 * 0);
// //compute ((⇓ (⇧ (((((((((((((H0l' + H1l') + H2l') + H3l') + H4l') + H5l') + H6l') + H7l') + H8l') + H9l') + H10l') + H11l') + H12l') + H13l'))));
// apply ⊤ᵢ
// end;