lia

lia.lp

require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.Eq Stdlib.Pos Stdlib.Bool;



inductive ℤ : TYPE ≔ // \BbbZ
| Z0 : ℤ
| Zpos : ℙ → ℤ
| Zneg : ℙ → ℤ;

constant symbol int : Set;

rule τ int ↪ ℤ;

print ℙ;


//symbol 1 ≔ Zpos Z0;

// boolean functions for testing head constructor
// Unary opposite

symbol ~ : ℤ → ℤ;
notation ~ prefix 24;

rule ~ Z0 ↪ Z0
with ~ (Zpos $p) ↪ Zneg $p
with ~ (Zneg $p) ↪ Zpos $p;

symbol ~_idem z : π (~ ~ z = z) ≔
begin
  induction { reflexivity; } { reflexivity; } { reflexivity; }
end;

symbol double : ℤ → ℤ;

rule double Z0 ↪ Z0
with double (Zpos $p) ↪ Zpos (O $p)
with double (Zneg $p) ↪ Zneg (O $p);

symbol succ_double : ℤ → ℤ;

rule succ_double Z0 ↪ Zpos H
with succ_double (Zpos $p) ↪ Zpos (I $p)
with succ_double (Zneg $p) ↪ Zneg (pos_pred_double $p);

symbol pred_double : ℤ → ℤ;

rule pred_double Z0 ↪ Zneg H
with pred_double (Zpos $p) ↪ Zpos (pos_pred_double $p)
with pred_double (Zneg $p) ↪ Zneg (I $p);

symbol sub : ℙ → ℙ → ℤ;

rule sub (I $p) (I $q) ↪ double (sub $p $q)
with sub (I $p) (O $q) ↪ succ_double (sub $p $q)
with sub (I $p) H      ↪ Zpos (O $p)
with sub (O $p) (I $q) ↪ pred_double (sub $p $q)
with sub (O $p) (O $q) ↪ double (sub $p $q)
with sub (O $p) H      ↪ Zpos (pos_pred_double $p)
with sub H      (I $q) ↪ Zneg (O $q)
with sub H      (O $q) ↪ Zneg (pos_pred_double $q)
with sub H       H     ↪ Z0;


symbol + : ℤ → ℤ → ℤ;
notation + infix left 20;

rule Z0      + $y      ↪ $y
with $x      + Z0      ↪ $x
with Zpos $x + Zpos $y ↪ Zpos (add $x $y)
with Zpos $x + Zneg $y ↪ sub $x $y
with Zneg $x + Zpos $y ↪ sub $y $x
with Zneg $x + Zneg $y ↪ Zneg (add $x $y);

symbol +1 x ≔ x + Zpos H;

builtin "0" ≔ Z0;
builtin "+1" ≔ +1;

require open Stdlib.Comp;

symbol ≐ : ℤ → ℤ → Comp; notation ≐ infix 12; // \doteq

rule Z0      ≐ Z0      ↪ Eq
with Z0      ≐ Zpos _  ↪ Lt
with Z0      ≐ Zneg _  ↪ Gt
with Zpos _  ≐ Z0      ↪ Gt
with Zpos $p ≐ Zpos $q ↪ compare $p $q
with Zpos _  ≐ Zneg _  ↪ Gt
with Zneg _  ≐ Z0      ↪ Lt
with Zneg _  ≐ Zpos _  ↪ Lt
with Zneg $p ≐ Zneg $q ↪ compare $q $p;

symbol ≤ [a] : τ a → τ a → Prop;
notation ≤ infix 10;

symbol < [a] : τ a → τ a → Prop;
notation < infix 10;

symbol ≥ [a] : τ a → τ a → Prop;
notation ≥ infix 10;

symbol > [a] : τ a → τ a → Prop;
notation > infix 10;


symbol - x y ≔ x + ~ y;
notation - infix left 20;

symbol sub_same z : π (sub z z = Z0) ≔
begin
  induction
   { assume x xrec; simplify; rewrite xrec; reflexivity; }
   { assume x xrec; simplify; rewrite xrec; reflexivity; }
   { reflexivity; }
end;

symbol -_same z : π (z + ~ z = 0) ≔
begin
  induction
   { reflexivity; }
   { simplify; refine sub_same; }
   { simplify; refine sub_same; }
end;

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

symbol f: τ int → τ int;

symbol o: Set;
rule τ o ↪ Prop;



symbol ∨ : Prop → Prop → Prop; // \/ or \vee

notation ∨ infix left 6;

constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
constant symbol ∨ᵢ₂ [p q] : π q → π (p ∨ q);
symbol ∨ₑ [p q r] : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;


rule (¬ $x) ∨ (¬ $y) ↪ ¬ ($x ∧ $y);
rule ($x ⇒ ⊥) ∨ ($y ⇒ ⊥) ↪ ¬ ($x ∧ $y);

// symbol ~_>_to_≥  x y : π (¬ (x > y) = (x ≥ y)) ≔
// begin
//   assume x y;
  

// end;



symbol swap_> x y : π ((x > y) = ((x - y) > 0));
symbol swap_= x y : π ((x = y) = ((x - y) = 0));

symbol contradict [P Q: Prop]: π P → π (¬ P) → π Q;
symbol contrapos p q : π (p ⇒ q) → π (¬ q) → π (¬ p);
symbol nnpp p : π (¬ ¬ p) → π (p);

// symbol lia: π (¬ (f a > f b) ∨  ¬ (f a = f b)) ≔
// begin
//   simplify;
//   assume H;
//   have H1:  π (f a > f b) { apply ∧ₑ₁ H };
//   have H2:  π (f a = f b) { apply ∧ₑ₂ H };

//   //rewrite swap_> (f a) (f b);
//   //rewrite swap_= (f a) (f b);
//   //apply nnpp;
//   admit
// end;


symbol x: τ int;
symbol y: τ int;
symbol z: τ int;

symbol × : ℤ → ℤ → ℤ;
notation × infix left 22;

rule 0       × _       ↪ 0
with _       × 0       ↪ 0
with Zpos $x × Zpos $y ↪ Zpos (mul $x $y)
with Zpos $x × Zneg $y ↪ Zneg (mul $x $y)
with Zneg $x × Zpos $y ↪ Zneg (mul $x $y)
with Zneg $x × Zneg $y ↪ Zpos (mul $x $y);


symbol Z_plus_gt_compat x y p q : π (x > y) → π (p > q) → π (x + p > y + q);
// we use the addition property with p in the first inequality H1 : (x + p > y + p)
// we use the addition property with y in the second inequality
// H2: p + y > q + y
// symmetry on (y + p) in H1
// transitivity give x + p > p + y > q + y
// commutatitve property of sum give  x + p > y + q

symbol Z_sub_compat x y p q : π (x > y) → π (p < q) → π (x - p > y - q);

symbol Zgt_irrefl (n: τ int) : π (¬ (n > n));


symbol lia2: π (
  ¬ (2 × x - y + z > 0)
  ∨  ¬ ((~ x) + y - z > 0)
  ∨  ¬ (~ y + z > 0)) ≔
begin
  simplify;
  assume H;
  have H1: π (2 × x - y + z > 0) { apply ∧ₑ₁ (∧ₑ₁ H); };
  have H2: π ((~ x) + y - z > 0) { apply ∧ₑ₂ (∧ₑ₁ H); };
  have H3: π ((~ y + z > 0)) { apply (∧ₑ₂ H) };
  have H4: π ((((2 × x) - y) + z) + ((~ x + y) - z) > 0) {
    apply Z_plus_gt_compat (2 × x - y + z) 0 ((~ x) + y - z) 0 H1 H2
  };
  have H5: π ((((2 × x) - y) + z) + ((~ x + y) - z) + (~ y + z) > 0) {
    apply Z_plus_gt_compat
      ((((2 × x) - y) + z) + ((~ x + y) - z))
      0
      (~ y + z)
      0
      H4
      H3
  };
  have H6: π ((((((2 × x) - y) + z) + ((~ x + y) - z)) + (~ y + z)) = 0) {
    simplify;
    admit
  };
  have H7: π (0 > 0) {
    rewrite left .[x in x > _] H6;
    apply H5;
  };
  apply Zgt_irrefl 0 H7;
end;

associative commutative symbol ⩲: τ int → τ int → τ int; notation ⩲ infix right 3;
associative commutative symbol ⨱: τ int → τ int → τ int; notation ⨱ infix right 4;

assert (x y w z : τ int) ⊢ x ⩲ (~ x) ⩲ (y ⨱ w) ⩲ z ≡ z ⩲ x ⩲ (w ⨱ y) ⩲ (~ x);

// RING =====

//
// inductive Ring: TYPE ≔
// | 𝟘: Ring
// | 𝟙: Ring
// | ⨁: Ring → Ring → Ring
// | ⨂: Ring → Ring → Ring
// | ⨪: Ring → Ring
// ;
// notation ⨁ infix left 3;
// notation ⨂ infix left 4;

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

symbol 𝟘: τ ring;
symbol 𝟙: τ ring;
symbol ⨁ : τ ring → τ ring → τ ring; notation ⨁ infix right 3;
symbol ⨂ : τ ring → τ ring → τ ring; notation ⨂ infix right 4;
symbol ⨪ : τ ring → τ ring; notation ⨪ prefix 2;

symbol ind_Ring : Π p0: (Ring → Prop), π (p0 𝟘) → π (p0 𝟙) → (Π x0: Ring, π (p0 x0) → Π x1: Ring, π (p0 x1) → π (p0 (x0 ⨁ x1))) → (Π x0: Ring, π (p0 x0) → Π x1: Ring, π (p0 x1) → π (p0 (x0 ⨂ x1))) → (Π x0: Ring, π (p0 x0) → π (p0 (⨪ x0))) → Π x: Ring, π (p0 x);
rule ind_Ring $0 $1 $2 $3 $4 $5 𝟘 ↪ $1
with ind_Ring $0 $1 $2 $3 $4 $5 𝟙 ↪ $2
with ind_Ring $0 $1 $2 $3 $4 $5 ($6 ⨁ $7) ↪ $3 $6 (ind_Ring $0 $1 $2 $3 $4 $5 $6) $7 (ind_Ring $0 $1 $2 $3 $4 $5 $7)
with ind_Ring $0 $1 $2 $3 $4 $5 ($6 ⨂ $7) ↪ $4 $6 (ind_Ring $0 $1 $2 $3 $4 $5 $6) $7 (ind_Ring $0 $1 $2 $3 $4 $5 $7)
with ind_Ring $0 $1 $2 $3 $4 $5 (⨪ $6) ↪ $5 $6 (ind_Ring $0 $1 $2 $3 $4 $5 $6);

symbol a : τ ring;
symbol b : τ ring;
symbol c : τ ring;

assert ⊢ a ⨁ b ⨁ c ≡ a ⨁ (b ⨁ c);

// ==========

rule 𝟘 ⨁ $x ↪ $x
with (⨪ $x) ⨁ $x ↪ 𝟘
with ($x ⨁ $y) ⨁ $z ↪ $x ⨁ ($y ⨁ $z)
with (⨪ $x) ⨁ ($x ⨁ $y) ↪ $y
with $x ⨁ 𝟘 ↪ $x
with  ⨪ 𝟘 ↪ 𝟘
with ⨪ (⨪ $x) ↪ $x
with $x ⨁ (⨪ $x) ↪ 𝟘
with $x ⨁ ((⨪ $x) ⨁ $y) ↪ $y
with ⨪ ($x ⨁ $y) ↪ (⨪ $x) ⨁ (⨪ $y);

// rule $x ⨁ 𝟘 ↪ $x
// with $x ⨁ (⨪ $x) ↪ 𝟘
// with ⨪ 𝟘 ↪ 𝟘
// with ⨪ (⨪ $x) ↪ $x
// with ⨪ ($x ⨁ $y) ↪ (⨪ $x) ⨁ (⨪ $y)
// with ($x ⨁ $y) ⨁ $z ↪ $x ⨁ ($y ⨁ $z)

rule $x ⨂ ($y ⨁ $z) ↪ ($x ⨂ $y) ⨁ ($x ⨂ $z) 
with 𝟘 ⨂ $x ↪ 𝟘
with $x ⨂ (⨪ $y) ↪ ⨪ ($x ⨂ $y)
with 𝟙 ⨂ $x ↪ $x
with ($x ⨂ $y) ⨂ $z ↪ $x ⨂ ($y ⨂ $z)
;

assert ⊢ a ⨁ b ⨁ c ≡ (a ⨁ b) ⨁ c;


// ORDER for a b c
// Let pick the order c ≥ - c > b ≥ - b > a ≥ - a > 1 > 0
// same with constant 

//commutativity for 0 and 1

rule c ⨁ 𝟘 ↪ 𝟘 ⨁ c;
rule b ⨁ 𝟘 ↪ 𝟘 ⨁ b;
rule a ⨁ 𝟘 ↪ 𝟘 ⨁ a;
rule 𝟙 ⨁ 𝟘 ↪ 𝟘 ⨁ 𝟙;

rule c ⨁ 𝟙 ↪ 𝟙 ⨁ c;
rule b ⨁ 𝟙 ↪ 𝟙 ⨁ b;
rule a ⨁ 𝟙 ↪ 𝟙 ⨁ a;

rule c ⨂ 𝟘 ↪ 𝟘 ⨂ c;
rule b ⨂ 𝟘 ↪ 𝟘 ⨂ b;
rule a ⨂ 𝟘 ↪ 𝟘 ⨂ a;
rule 𝟙 ⨂ 𝟘 ↪ 𝟘 ⨂ 𝟙;

rule c ⨂ 𝟙 ↪ 𝟙 ⨂ c;
rule b ⨂ 𝟙 ↪ 𝟙 ⨂ b;
rule a ⨂ 𝟙 ↪ 𝟙 ⨂ a;

//commutativity for ⨁
rule c ⨁ a ↪ a ⨁ c;
rule c ⨁ b ↪ b ⨁ c;  
rule b ⨁ a ↪ a ⨁ b;
rule b ⨁ (⨪ a) ↪ (⨪ a) ⨁ b;

rule (⨪ c) ⨁ a     ↪ a ⨁ (⨪ c);
rule (⨪ c) ⨁ (⨪ a) ↪ (⨪ a) ⨁ (⨪ c);
rule (⨪ c) ⨁ b     ↪ b ⨁ (⨪ c);
rule (⨪ c) ⨁ (⨪ b) ↪ (⨪ b) ⨁ (⨪ c);
rule (⨪ b) ⨁ a     ↪ a ⨁ (⨪ b);
rule (⨪ b) ⨁ (⨪ a) ↪ (⨪ a) ⨁ (⨪ b);

// Assoc for ⨁
rule c ⨁ (b ⨁ $x)     ↪ b ⨁ (c ⨁ $x);
rule c ⨁ ((⨪ b) ⨁ $x) ↪ (⨪ b) ⨁ (c ⨁ $x);
rule c ⨁ (a ⨁ $x)     ↪ a ⨁ (c ⨁ $x);
rule c ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ (c ⨁ $x);
rule b ⨁ (a ⨁ $x)     ↪ a ⨁ (b ⨁ $x);
rule b ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ (b ⨁ $x);

rule (⨪ c) ⨁ (b ⨁ $x)     ↪ b ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ ((⨪ b) ⨁ $x) ↪ (⨪ b) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ (a ⨁ $x)     ↪ a ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ b) ⨁ (a ⨁ $x)     ↪ a ⨁ ((⨪ b) ⨁ $x);
rule (⨪ b) ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ ((⨪ b) ⨁ $x);


//commutativity for ⨂
rule c ⨂ a ↪ a ⨂ c;
rule c ⨂ b ↪ b ⨂ c;  
rule b ⨂ a ↪ a ⨂ b;
rule b ⨂ (⨪ a) ↪ (⨪ a) ⨂ b;

rule (⨪ c) ⨂ a     ↪ a ⨂ (⨪ c);
rule (⨪ c) ⨂ (⨪ a) ↪ (⨪ a) ⨂ (⨪ c);
rule (⨪ c) ⨂ b     ↪ b ⨂ (⨪ c);
rule (⨪ c) ⨂ (⨪ b) ↪ (⨪ b) ⨂ (⨪ c);
rule (⨪ b) ⨂ a     ↪ a ⨂ (⨪ b);
rule (⨪ b) ⨂ (⨪ a) ↪ (⨪ a) ⨂ (⨪ b);

// Assoc for ⨂
rule c ⨂ (b ⨂ $x)     ↪ b ⨂ (c ⨂ $x);
rule c ⨂ ((⨪ b) ⨂ $x) ↪ (⨪ b) ⨂ (c ⨂ $x);
rule c ⨂ (a ⨂ $x)     ↪ a ⨂ (c ⨂ $x);
rule c ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ (c ⨂ $x);
rule b ⨂ (a ⨂ $x)     ↪ a ⨂ (b ⨂ $x);
rule b ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ (b ⨂ $x);

rule (⨪ c) ⨂ (b ⨂ $x)     ↪ b ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ ((⨪ b) ⨂ $x) ↪ (⨪ b) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ (a ⨂ $x)     ↪ a ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ b) ⨂ (a ⨂ $x)     ↪ a ⨂ ((⨪ b) ⨂ $x);
rule (⨪ b) ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ ((⨪ b) ⨂ $x);

assert ⊢ 𝟙 ⨁ (⨪ b) ⨁ (b ⨁ (c ⨁ 𝟘 ⨁ (b ⨁ a))) ⨁ (⨪ b) ⨁ (⨪ c) ⨁ (⨪ a) ≡ 𝟙;

//compute 𝟙 ⨁ (⨪ b) ⨁ (b ⨁ (c ⨁ 𝟘 ⨁ (b ⨁ a))) ⨁ (⨪ b) ⨁ (⨪ c) ⨁ (⨪ a);

symbol const: τ int → τ ring;

// Rule for computations of polynom and constant (degree 1 for now)
rule (const $a) ⨁ (const $b)     ↪ const ($a + $b)
with (const $a) ⨁ (⨪ (const $b)) ↪ const ($a - $b)
with (⨪ (const $a)) ⨁ (const $b) ↪ const (~ $a + $b)

with (const $a) ⨂ (const $b)     ↪ const ($a × $b)
with (const $a) ⨂ (⨪ (const $b)) ↪ const (~ ($a × $b))
with (⨪ (const $a)) ⨂ (const $b) ↪ const (~ ($a × $b))
;

// a*x ⋈ b*x -> a ⋈ b x
rule ((const $c) ⨂ $a) ⨁ ((const $d) ⨂ $a)     ↪ ((const ($c + $d)) ⨂ $a)
with ((const $c) ⨂ $a) ⨁ ⨪ ((const $d) ⨂ $a)   ↪ ((const ($c + (~ $d))) ⨂ $a)
with (⨪ ((const $c) ⨂ $a)) ⨁ ((const $d) ⨂ $a) ↪ ((const ((~ $c) + $d)) ⨂ $a)
with ((const $c) ⨂ $a) ⨁ $a                    ↪ ((const ($c + 1)) ⨂ $a)
with ((const $c) ⨂ $a) ⨁ (⨪ $a)                ↪ ((const ($c - 1)) ⨂ $a)
with (⨪ ((const $c) ⨂ $a)) ⨁ $a                    ↪ ((const ((~ $c) + 1)) ⨂ $a)
with (⨪ ((const $c) ⨂ $a)) ⨁ (⨪ $a)                ↪ ((const ((~ $c) - 1)) ⨂ $a)
with $a ⨁ ((const $c) ⨂ $a)                    ↪ ((const ($c + 1)) ⨂ $a)
with (⨪ $a) ⨁ ((const $c) ⨂ $a)                ↪ ((const ((~ 1) + $c)) ⨂ $a)
with $a ⨁ ⨪ ((const $c) ⨂ $a)                    ↪ ((const (1 + (~ $c))) ⨂ $a)
with (⨪ $a) ⨁ ⨪ ((const $c) ⨂ $a)                ↪ ((const ((~ 1) + ~ $c)) ⨂ $a)
;

rule (const 0) ↪ 𝟘;
rule (const (Zpos H)) ↪ 𝟙;

// Commutativity ⨁ with constant
rule c ⨁ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨁ c
with c ⨁ (const $c ⨂ b) ↪ (const $c ⨂ b) ⨁ c
with b ⨁ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨁ b

with (const $d ⨂ c) ⨁ a ↪ a ⨁ (const $d ⨂ c)
with (const $d ⨂ c) ⨁ b ↪ b ⨁ (const $d ⨂ c)
with (const $d ⨂ b) ⨁ a ↪ a ⨁ (const $d ⨂ b)

with (const $d ⨂ c) ⨁ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨁ (const $d ⨂ c)
with (const $d ⨂ c) ⨁ (const $c ⨂ b) ↪ (const $c ⨂ b) ⨁ (const $d ⨂ c)
with (const $d ⨂ b) ⨁ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨁ (const $d ⨂ b)
;

rule (⨪ (const $c ⨂ c)) ⨁ a     ↪ a ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨁ (⨪ a) ↪ (⨪ a) ⨁ (⨪ (const $c ⨂ c));
rule(⨪ (const $c ⨂ c)) ⨁ b      ↪ b ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨁ (⨪ b) ↪ (⨪ b) ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ b)) ⨁ a     ↪ a ⨁ (⨪ (const $c ⨂ b));
rule (⨪ (const $c ⨂ b)) ⨁ (⨪ a) ↪ (⨪ a) ⨁ (⨪ (const $c ⨂ b));

rule (⨪ (const $c ⨂ c)) ⨁ (const $d ⨂ a)     ↪ (const $d ⨂ a) ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨁ (⨪ (const $d ⨂ a)) ↪ (⨪ (const $d ⨂ a)) ⨁ (⨪ (const $c ⨂ c));
rule(⨪ (const $c ⨂ c)) ⨁ (const $d ⨂ b)      ↪ (const $d ⨂ b) ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨁ (⨪ (const $d ⨂ b)) ↪ (⨪ (const $d ⨂ b)) ⨁ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ b)) ⨁ (const $d ⨂ a)     ↪ (const $d ⨂ a) ⨁ (⨪ (const $c ⨂ b));
rule (⨪ (const $c ⨂ b)) ⨁ (⨪ (const $d ⨂ a)) ↪ (⨪ (const $d ⨂ a)) ⨁ (⨪ (const $c ⨂ b));


// Associativity ⨁ with constant

rule c ⨁ ((const $c ⨂ b) ⨁ $x)     ↪  (const $c ⨂ b) ⨁ (c ⨁ $x);
rule c ⨁ ((⨪  (const $c ⨂ b)) ⨁ $x) ↪ (⨪ (const $c ⨂ b)) ⨁ (c ⨁ $x);
rule c ⨁ ( (const $c ⨂ a) ⨁ $x)     ↪  (const $c ⨂ a) ⨁ (c ⨁ $x);
rule c ⨁ ((⨪  (const $c ⨂ a)) ⨁ $x) ↪ (⨪  (const $c ⨂ a)) ⨁ (c ⨁ $x);
rule b ⨁ ((const $c ⨂ a) ⨁ $x)     ↪ (const $c ⨂ a) ⨁ (b ⨁ $x);
rule b ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x) ↪ (⨪ (const $c ⨂ a)) ⨁ (b ⨁ $x);

rule (⨪ c) ⨁ ((const $c ⨂ b) ⨁ $x)     ↪ (const $c ⨂ b) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ ((⨪ (const $c ⨂ b)) ⨁ $x) ↪ (⨪ (const $c ⨂ b)) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ ((const $c ⨂ a) ⨁ $x)     ↪ (const $c ⨂ a) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ c) ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x) ↪ (⨪ (const $c ⨂ a)) ⨁ ((⨪ c) ⨁ $x);
rule (⨪ b) ⨁ ((const $c ⨂ a) ⨁ $x)     ↪ (const $c ⨂ a) ⨁ ((⨪ b) ⨁ $x);
rule (⨪ b) ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x) ↪ (⨪ (const $c ⨂ a)) ⨁ ((⨪ b) ⨁ $x);

rule (const $d ⨂ c) ⨁ ((const $c ⨂ b) ⨁ $x)      ↪  (const $c ⨂ b) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ((⨪  (const $c ⨂ b)) ⨁ $x) ↪ (⨪ (const $c ⨂ b)) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ( (const $c ⨂ a) ⨁ $x)     ↪  (const $c ⨂ a) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ((⨪  (const $c ⨂ a)) ⨁ $x) ↪ (⨪  (const $c ⨂ a)) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ b) ⨁ ((const $c ⨂ a) ⨁ $x)      ↪ (const $c ⨂ a) ⨁ ((const $d ⨂ b) ⨁ $x);
rule (const $d ⨂ b) ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x)  ↪ (⨪ (const $c ⨂ a)) ⨁ ((const $d ⨂ b) ⨁ $x);

rule (⨪ (const $d ⨂ c)) ⨁ ((const $c ⨂ b) ⨁ $x)     ↪ (const $c ⨂ b) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ ((⨪ (const $c ⨂ b)) ⨁ $x) ↪ (⨪ (const $c ⨂ b)) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ ((const $c ⨂ a) ⨁ $x)     ↪ (const $c ⨂ a) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x) ↪ (⨪ (const $c ⨂ a)) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ b)) ⨁ ((const $c ⨂ a) ⨁ $x)     ↪ (const $c ⨂ a) ⨁ ((⨪ (const $d ⨂ b)) ⨁ $x);
rule (⨪ (const $d ⨂ b)) ⨁ ((⨪ (const $c ⨂ a)) ⨁ $x) ↪ (⨪ (const $c ⨂ a)) ⨁ ((⨪ (const $d ⨂ b)) ⨁ $x);

rule (const $d ⨂ c) ⨁ (b ⨁ $x)      ↪  b ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ((⨪  b) ⨁ $x) ↪ (⨪ b) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ( a ⨁ $x)     ↪  a ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ c) ⨁ ((⨪  a) ⨁ $x) ↪ (⨪  a) ⨁ ((const $d ⨂ c) ⨁ $x);
rule (const $d ⨂ b) ⨁ (a ⨁ $x)      ↪ a ⨁ ((const $d ⨂ b) ⨁ $x);
rule (const $d ⨂ b) ⨁ ((⨪ a) ⨁ $x)  ↪ (⨪ a) ⨁ ((const $d ⨂ b) ⨁ $x);

rule (⨪ (const $d ⨂ c)) ⨁ (b ⨁ $x)     ↪ b ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ ((⨪ b) ⨁ $x) ↪ (⨪ b) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ (a ⨁ $x)     ↪ a ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ c)) ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ ((⨪ (const $d ⨂ c)) ⨁ $x);
rule (⨪ (const $d ⨂ b)) ⨁ (a ⨁ $x)     ↪ a ⨁ ((⨪ (const $d ⨂ b)) ⨁ $x);
rule (⨪ (const $d ⨂ b)) ⨁ ((⨪ a) ⨁ $x) ↪ (⨪ a) ⨁ ((⨪ (const $d ⨂ b)) ⨁ $x);


// Commutativity ⨂ with constant

rule c ⨂ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨂ c
with c ⨂ (const $c ⨂ b) ↪ (const $c ⨂ b) ⨂ c
with b ⨂ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨂ b

with (const $d ⨂ c) ⨂ a ↪ a ⨂ (const $d ⨂ c)
with (const $d ⨂ c) ⨂ b ↪ b ⨂ (const $d ⨂ c)
with (const $d ⨂ b) ⨂ a ↪ a ⨂ (const $d ⨂ b)

with (const $d ⨂ c) ⨂ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨂ (const $d ⨂ c)
with (const $d ⨂ c) ⨂ (const $c ⨂ b) ↪ (const $c ⨂ b) ⨂ (const $d ⨂ c)
with (const $d ⨂ b) ⨂ (const $c ⨂ a) ↪ (const $c ⨂ a) ⨂ (const $d ⨂ b)
;

rule (⨪ (const $c ⨂ c)) ⨂ a     ↪ a ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨂ (⨪ a) ↪ (⨪ a) ⨂ (⨪ (const $c ⨂ c));
rule(⨪ (const $c ⨂ c)) ⨂ b      ↪ b ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨂ (⨪ b) ↪ (⨪ b) ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ b)) ⨂ a     ↪ a ⨂ (⨪ (const $c ⨂ b));
rule (⨪ (const $c ⨂ b)) ⨂ (⨪ a) ↪ (⨪ a) ⨂ (⨪ (const $c ⨂ b));

rule (⨪ (const $c ⨂ c)) ⨂ (const $d ⨂ a)     ↪ (const $d ⨂ a) ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨂ (⨪ (const $d ⨂ a)) ↪ (⨪ (const $d ⨂ a)) ⨂ (⨪ (const $c ⨂ c));
rule(⨪ (const $c ⨂ c)) ⨂ (const $d ⨂ b)      ↪ (const $d ⨂ b) ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ c)) ⨂ (⨪ (const $d ⨂ b)) ↪ (⨪ (const $d ⨂ b)) ⨂ (⨪ (const $c ⨂ c));
rule (⨪ (const $c ⨂ b)) ⨂ (const $d ⨂ a)     ↪ (const $d ⨂ a) ⨂ (⨪ (const $c ⨂ b));
rule (⨪ (const $c ⨂ b)) ⨂ (⨪ (const $d ⨂ a)) ↪ (⨪ (const $d ⨂ a)) ⨂ (⨪ (const $c ⨂ b));


// Associativity ⨂ with constant

rule c ⨂ ((const $c ⨂ b) ⨂ $x)     ↪  (const $c ⨂ b) ⨂ (c ⨂ $x);
rule c ⨂ ((⨪  (const $c ⨂ b)) ⨂ $x) ↪ (⨪ (const $c ⨂ b)) ⨂ (c ⨂ $x);
rule c ⨂ ( (const $c ⨂ a) ⨂ $x)     ↪  (const $c ⨂ a) ⨂ (c ⨂ $x);
rule c ⨂ ((⨪  (const $c ⨂ a)) ⨂ $x) ↪ (⨪  (const $c ⨂ a)) ⨂ (c ⨂ $x);
rule b ⨂ ((const $c ⨂ a) ⨂ $x)     ↪ (const $c ⨂ a) ⨂ (b ⨂ $x);
rule b ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x) ↪ (⨪ (const $c ⨂ a)) ⨂ (b ⨂ $x);

rule (⨪ c) ⨂ ((const $c ⨂ b) ⨂ $x)     ↪ (const $c ⨂ b) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ ((⨪ (const $c ⨂ b)) ⨂ $x) ↪ (⨪ (const $c ⨂ b)) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ ((const $c ⨂ a) ⨂ $x)     ↪ (const $c ⨂ a) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ c) ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x) ↪ (⨪ (const $c ⨂ a)) ⨂ ((⨪ c) ⨂ $x);
rule (⨪ b) ⨂ ((const $c ⨂ a) ⨂ $x)     ↪ (const $c ⨂ a) ⨂ ((⨪ b) ⨂ $x);
rule (⨪ b) ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x) ↪ (⨪ (const $c ⨂ a)) ⨂ ((⨪ b) ⨂ $x);


rule (const $d ⨂ c) ⨂ ((const $c ⨂ b) ⨂ $x)      ↪  (const $c ⨂ b) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ ((⨪  (const $c ⨂ b)) ⨂ $x) ↪ (⨪ (const $c ⨂ b)) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ ( (const $c ⨂ a) ⨂ $x)     ↪  (const $c ⨂ a) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ ((⨪  (const $c ⨂ a)) ⨂ $x) ↪ (⨪  (const $c ⨂ a)) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ b) ⨂ ((const $c ⨂ a) ⨂ $x)      ↪ (const $c ⨂ a) ⨂ ((const $d ⨂ b) ⨂ $x);
rule (const $d ⨂ b) ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x)  ↪ (⨪ (const $c ⨂ a)) ⨂ ((const $d ⨂ b) ⨂ $x);

rule (⨪ (const $d ⨂ c)) ⨂ ((const $c ⨂ b) ⨂ $x)     ↪ (const $c ⨂ b) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ ((⨪ (const $c ⨂ b)) ⨂ $x) ↪ (⨪ (const $c ⨂ b)) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ ((const $c ⨂ a) ⨂ $x)     ↪ (const $c ⨂ a) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x) ↪ (⨪ (const $c ⨂ a)) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ b)) ⨂ ((const $c ⨂ a) ⨂ $x)     ↪ (const $c ⨂ a) ⨂ ((⨪ (const $d ⨂ b)) ⨂ $x);
rule (⨪ (const $d ⨂ b)) ⨂ ((⨪ (const $c ⨂ a)) ⨂ $x) ↪ (⨪ (const $c ⨂ a)) ⨂ ((⨪ (const $d ⨂ b)) ⨂ $x);

rule (const $d ⨂ c) ⨂ (b ⨂ $x)      ↪  b ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ ((⨪  b) ⨂ $x) ↪ (⨪ b) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ (a ⨂ $x)     ↪  a ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ c) ⨂ ((⨪  a) ⨂ $x) ↪ (⨪ a) ⨂ ((const $d ⨂ c) ⨂ $x);
rule (const $d ⨂ b) ⨂ (a ⨂ $x)      ↪ a ⨂ ((const $d ⨂ b) ⨂ $x);
rule (const $d ⨂ b) ⨂ ((⨪ a) ⨂ $x)  ↪ (⨪ a) ⨂ ((const $d ⨂ b) ⨂ $x);

rule (⨪ (const $d ⨂ c)) ⨂ (b ⨂ $x)     ↪ b ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ ((⨪ b) ⨂ $x) ↪ (⨪ b) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ (a ⨂ $x)     ↪ a ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ c)) ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ ((⨪ (const $d ⨂ c)) ⨂ $x);
rule (⨪ (const $d ⨂ b)) ⨂ (a ⨂ $x)     ↪ a ⨂ ((⨪ (const $d ⨂ b)) ⨂ $x);
rule (⨪ (const $d ⨂ b)) ⨂ ((⨪ a) ⨂ $x) ↪ (⨪ a) ⨂ ((⨪ (const $d ⨂ b)) ⨂ $x);

assert ⊢ ((const 2 ⨂ a) ⨁ (⨪ b) ⨁ c) ⨁ ((⨪ (const 2 ⨂ a)) ⨁ (const 2 ⨂ b) ⨁ (⨪ (const 2 ⨂ c))) ⨁ ((⨪ b) ⨁ c) ≡ 𝟘;

assert ⊢ (⨪ b) ⨁ (b ⨁ (c ⨁ 𝟘 ⨁ (b ⨁ a))) ⨁ (⨪ b) ⨁ (⨪ c) ⨁ (⨪ a) ≡ 𝟘;

symbol T_ring : τ int → τ ring;
rule T_ring 0 ↪ 𝟘
with T_ring (Zpos H) ↪ 𝟙
with T_ring ($x + $y) ↪ T_ring $x ⨁ T_ring $y
with T_ring ($x × $y) ↪ T_ring $x ⨂ T_ring $y
with T_ring (~ $x) ↪ ⨪ T_ring $x
with T_ring (Zpos $x) ↪ const (Zpos $x)
with T_ring x ↪ a
with T_ring y ↪ b
with T_ring z ↪ c;

//compute (T_ring (x + y - x));
//compute T_ring (((2 × x) - y + z) + ((~ (2 × x)) + (2 × y) - (2 × z)) + ((~ y) + z));

//compute T_ring (2 × ((~ x) + y - z));

symbol compat_lt_mult c a b : π (c > 0) → π (a > b) → π (c × a > c × b) ;

// Reflexivity theorem
symbol ring_correct [a b: τ int] : π (T_ring a =  T_ring b) → π (a = b);

symbol lia3: π (
  ¬ ((2 × x) - y + z > 0)
  ∨  ¬ ((~ x) + y - z > 0)
  ∨  ¬ (~ y + z > 0)) ≔
begin
  simplify;
  assume H;
  have H1: π (2 × x - y + z > 0) { apply ∧ₑ₁ (∧ₑ₁ H); };
  have H2: π ((~ x) + y - z > 0) { apply ∧ₑ₂ (∧ₑ₁ H); };
  have H3: π ((~ y + z > 0)) { apply (∧ₑ₂ H) };
  have H2': π (2 × ((~ x) + y - z) > 2 × 0) {  apply compat_lt_mult 2 ((~ x) + y - z) 0 { simplify; admit } { apply H2 } };
  have H4: π ((((2 × x) - y) + z) + (2 × ((~ x + y) - z)) > (2 × 0)) {
    apply Z_plus_gt_compat
      (2 × x - y + z) 0
      (2 × ((~ x + y) - z)) (2 × 0)
      H1 H2'
  };
  have H5: π (((((2 × x) - y) + z) + (2 × ((~ x + y) - z)) + (~ y + z)) > (2 × 0)) {
    apply Z_plus_gt_compat
      ((((2 × x) - y) + z) + (2 × ((~ x + y) - z)))
      (2 × 0)
      (~ y + z)
      0
      H4
      H3
  };
  have H6: π ((((((2 × x) - y) + z) + (2 × ((~ x + y) - z))) + (~ y + z)) = 0) {
    apply ring_correct;
    reflexivity
  };
  have H7: π (0 > 0) {
    rewrite left .[x in x > _] H6;
    apply H5;
  };
  apply Zgt_irrefl 0 H7;
end;


//compute (T_ring (1 + x + y - x - y));

//assert ⊢ b ⨁ (c ⨁ 𝟘 ⨁ (b ⨁ a)) ≡ c ⨁ (a ⨁ 𝟘 ⨁ (b ⨁ b) ⨁ 𝟘);

// symbol ≿ : τ ring → τ ring → τ bool;
// notation ≿ infix left 10;

// rule c ≿ a ↪ true
// with c ≿ b ↪ true
// with c ≿ c ↪ false
// with b ≿ c ↪ false
// with b ≿ b ↪ false
// with b ≿ a ↪ true
// with a ≿ $x ↪ false;

// constant symbol ⋈ : Set → Set → Set; notation ⋈ infix right 10; // \times
// symbol & [a b] : τ a → τ b → τ (a ⋈ b); notation & infix right 30;

// symbol if : 𝔹 → Π [a], τ a → τ a → τ a;

// rule if true  $x _ ↪ $x
// with if false _ $y ↪ $y;

// //debug +tur;

// symbol U1  : τ bool → τ ring → τ ring → τ ring;
// rule U1 true $x $y ↪ $y ⨁ $x
// with U1 false $x $y ↪ $x ⨁ $y;

// compute U1 (c ≿ a) c a;

// type (c ≿ a);
// type (a ⨁ b);

// rule ($x ⨁ $y) ↪ U1 ($x ≿ $y) $x $y;

// debug +tur;

// compute (c ⨁ a);

// rule U₂ true ↪ 

//compute U₁ false (a ⨁ b);

//rule ($x ⨁ $y) ↪ U₁ ($x ≿ $y) ($x ⨁ $y);
// with U₁ true ($x ⨁ $y) ↪ ($y ⨁ $x)
// with U₁ false ($x ⨁ $y) ↪ ($x ⨁ $y);

//assert x y z  ⊢ x ⨁ y ⨁ z ≡ x ⨁ y ⨁ z;