Skip to content

Commit

Permalink
add error messages
Browse files Browse the repository at this point in the history 
* add more proofs
* fix parsing associativity
* print colored error messages to screen, many at once
* make more elements spanned
* move out function that checks one proof
  • Loading branch information
@optozorax
optozorax committed Jan 30, 2021
1 parent b7261c5 commit 9585374
Show file tree
Hide file tree
Showing 11 changed files with 814 additions and 307 deletions.
2 changes: 2 additions & 0 deletions Cargo.toml
View file
Expand Up @@ -11,3 +11,5 @@ peg = "0.6.3"
itertools = "0.9.0"
colored = "1.9.3"
petgraph = "0.5.1"
annotate-snippets = { version = "0.9.0", features = ["color"] }
thiserror = "1.0.23"
235 changes: 145 additions & 90 deletions fpl/math.fpl
View file
Expand Up @@ -2,14 +2,39 @@
1. (a+b)+c <-> a+(b+c);
2. a+b <-> b+a;
3. a+0 <-> a;
4. a+(b+c) <-> b+(a+c) {
a+(b+c);
^^^^^^^ sum.1r;
(a+b)+c;
.^^^ sum.2l;
(b+a)+c;
^^^^^^^ sum.1l;
};


[sub]
1. a+(-b) <-> a-b;
2. a-a <-> 0;
3. a+(b-c) <->b+(a-c);
3. a+(b-c) <-> b+(a-c) {
a+(b-c);
. ^^^ sub.1r;
a+(b+(-c));
^^^^^^^^^^ sum.4l;
b+(a+(-c));
. ^^^^^^ sub.1l;
};
4. a-b-c <-> a-(b+c);
5. 0 <-> -0;
6. a-(-b) <-> a+b;
7. a-b-c <-> a-c-b {
a-b-c;
^^^^^ sub.4l;
a-(b+c);
. ^^^ sum.2l;
a-(c+b);
^^^^^^^ sub.4r;
};


[mul]
1. (a*b)*c <-> a*(b*c);
Expand All @@ -25,54 +50,54 @@
2. a/0 <-> $undefined;
3. a*(b/c) <-> b*(a/c);
4. a/b/c <-> a/(b*c);
5. a <-> part(b = 0, a, a*b/b) {
a;
^ part.1r x := b = 0;
part(b = 0, a, a);
. ^ mul.3r;
part(b = 0, a, a*1);
. ^ part.2r else := $undefined;
part(b = 0, a, a*part($true, 1, $undefined));
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.4l;
part(not(b = 0), a*part($true, 1, $undefined), a);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.5l $f(x) := a*x;
part(not(b = 0), a*part($true & not(b = 0), 1, $undefined), a);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.4r;
part(b = 0, a, a*part($true & not(b = 0), 1, $undefined));
. ^^^^^^^^^^ neq.1r;
part(b = 0, a, a*part($true & b != 0, 1, $undefined));
. ^^^^^^^^^^^^^^ and.2l;
part(b = 0, a, a*part(b != 0 & $true, 1, $undefined));
. ^^^^^^^^^^^^^^ and.4l;
part(b = 0, a, a*part(b != 0, 1, $undefined));
. ^^^^^^^^^^^^^^^^^^^^^^^^^^^ div.1r;
5. a <-> part(b = 0, a, a*(b/b)) {
a;
^ part.1r x := b = 0;
part(b = 0, a, a);
. ^ mul.3r;
part(b = 0, a, a*1);
. ^ part.2r else := $undefined;
part(b = 0, a, a*part($true, 1, $undefined));
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.4l;
part(not(b = 0), a*part($true, 1, $undefined), a);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.5l $f(x) := a*x;
part(not(b = 0), a*part($true & not(b = 0), 1, $undefined), a);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.4r;
part(b = 0, a, a*part($true & not(b = 0), 1, $undefined));
. ^^^^^^^^^^ neq.1r;
part(b = 0, a, a*part($true & b != 0, 1, $undefined));
. ^^^^^^^^^^^^^^ and.2l;
part(b = 0, a, a*part(b != 0 & $true, 1, $undefined));
. ^^^^^^^^^^^^^^ and.4l;
part(b = 0, a, a*part(b != 0, 1, $undefined));
. ^^^^^^^^^^^^^^^^^^^^^^^^^^^ div.1r;
};

[muldiv]
1. a*(b+c) <-> a*b + a*c;
2. a*(b-c) <-> a*b - a*c {
a*(b-c);
. ^^^ sub.1r;
a*(b+(-c));
^^^^^^^^^^ muldiv.1l;
a*b+a*(-c);
. ^^^^^^ mul.2l;
a*b+(-c)*a;
. ^^^^^^ submul.1l;
a*b+(-c*a);
^^^^^^^^^^ sub.1l;
a*b-c*a;
. ^^^ mul.2l;
a*(b-c);
. ^^^ sub.1r;
a*(b+(-c));
^^^^^^^^^^ muldiv.1l;
a*b+a*(-c);
. ^^^^^^ mul.2l;
a*b+(-c)*a;
. ^^^^^^ submul.1l;
a*b+(-c*a);
^^^^^^^^^^ sub.1l;
a*b-c*a;
. ^^^ mul.2l;
};

[not]
1. not($true) <-> $false;
2. not(not(a)) <-> a;
3. $true <-> not($false) {
$true;
^^^^^ not.2r;
not(not($true));
. ^^^^^^^^^^ not.1l;
$true;
^^^^^ not.2r;
not(not($true));
. ^^^^^^^^^^ not.1l;
};

[eq]
Expand All @@ -82,20 +107,20 @@
[neq]
1. a != b <-> not(a = b);
2. a != b <-> b != a {
a != b;
^^^^^^ neq.1l;
not(a = b);
. ^^^^^ eq.1l;
not(b = a);
^^^^^^^^^^ neq.1r;
a != b;
^^^^^^ neq.1l;
not(a = b);
. ^^^^^ eq.1l;
not(b = a);
^^^^^^^^^^ neq.1r;
};
3. a != a <-> $false {
a != a;
^^^^^^ neq.1l;
not(a = a);
. ^^^^^ eq.2l;
not($true);
^^^^^^^^^^ not.1l;
a != a;
^^^^^^ neq.1l;
not(a = a);
. ^^^^^ eq.2l;
not($true);
^^^^^^^^^^ not.1l;
};

[and]
Expand All @@ -120,30 +145,30 @@
2. a < b <-> b > a;
3. a < b <-> not(a >= b);
4. a > b <-> not(a <= b) {
a > b;
^^^^^ ltgt.2r;
b < a;
^^^^^ ltgt.3l;
not(b >= a);
. ^^^^^^ ltgteq.2r;
a > b;
^^^^^ ltgt.2r;
b < a;
^^^^^ ltgt.3l;
not(b >= a);
. ^^^^^^ ltgteq.2r;
};

[ltgteq]
1. a <= b <-> (a < b) | (a = b);
2. a <= b <-> b >= a;
3. a <= a <-> $true {
a <= a;
^^^^^^ ltgteq.1l;
(a < a) | (a = a);
. ^^^^^ eq.2l;
(a < a) | $true;
^^^^^^^^^^^^^^^ or.5l;
a <= a;
^^^^^^ ltgteq.1l;
(a < a) | (a = a);
. ^^^^^ eq.2l;
(a < a) | $true;
^^^^^^^^^^^^^^^ or.5l;
};
4. a >= a <-> $true {
a >= a;
^^^^^^ ltgteq.2r;
a <= a;
^^^^^^ ltgteq.3l;
a >= a;
^^^^^^ ltgteq.2r;
a <= a;
^^^^^^ ltgteq.3l;
};

[abs]
Expand All @@ -166,31 +191,61 @@

[test]
1. 1*(2+6-5*(a-part(x >= 0, x, 0))) <-> part(x >= 0, 2+6-5*a+5*x, 2+6-5*a) {
1*(2+6-5*(a-part(x >= 0, x, 0)));
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.6l $f(x) := 1*(2+6-5*(a-x));
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a-0)));
. ^^^ sub.1r;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a+(-0))));
. ^^ sub.5r;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a+0)));
. ^^^ sum.3l;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*a));
. ^^^^^^^^^^^^^^^ mul.2l;
part(x >= 0, (2+6-5*(a-x))*1, 1*(2+6-5*a));
. ^^^^^^^^^^^^^^^ mul.3l;
part(x >= 0, 2+6-5*(a-x), 1*(2+6-5*a));
. ^^^^^^^^^^^ mul.2l;
part(x >= 0, 2+6-5*(a-x), (2+6-5*a)*1);
. ^^^^^^^^^^^ mul.3l;
part(x >= 0, 2+6-5*(a-x), 2+6-5*a);
. ^^^^^^^ muldiv.2l;
part(x >= 0, 2+6-(5*a-5*x), 2+6-5*a);
. ^^^^^^^ sub.1r;
part(x >= 0, 2+6-(5*a+(-5*x)), 2+6-5*a);
. ^^^^^^^^^^^^^^ sub.4r;
part(x >= 0, 2+6-5*a-(-5*x), 2+6-5*a);
. ^^^^^^^^^^ sub.6l;
1*(2+6-5*(a-part(x >= 0, x, 0)));
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ part.6l $f(x) := 1*(2+6-5*(a-x));
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a-0)));
. ^^^ sub.1r;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a+(-0))));
. ^^ sub.5r;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*(a+0)));
. ^^^ sum.3l;
part(x >= 0, 1*(2+6-5*(a-x)), 1*(2+6-5*a));
. ^^^^^^^^^^^^^^^ mul.2l;
part(x >= 0, (2+6-5*(a-x))*1, 1*(2+6-5*a));
. ^^^^^^^^^^^^^^^ mul.3l;
part(x >= 0, 2+6-5*(a-x), 1*(2+6-5*a));
. ^^^^^^^^^^^ mul.2l;
part(x >= 0, 2+6-5*(a-x), (2+6-5*a)*1);
. ^^^^^^^^^^^ mul.3l;
part(x >= 0, 2+6-5*(a-x), 2+6-5*a);
. ^^^^^^^ muldiv.2l;
part(x >= 0, 2+6-(5*a-5*x), 2+6-5*a);
. ^^^^^^^ sub.1r;
part(x >= 0, 2+6-(5*a+(-5*x)), 2+6-5*a);
. ^^^^^^^^^^^^^^^^ sub.4r;
part(x >= 0, 2+6-5*a-(-5*x), 2+6-5*a);
. ^^^^^^^^^^^^^^ sub.6l;
};

[unsafe]
1. a <-> b;

[polynoms_default]
1. (a-b)*(a+b) <-> a*a-b*b {
(a-b)*(a+b);
^^^^^^^^^^^ muldiv.1l;
(a-b)*a+(a-b)*b;
^^^^^^^ mul.2l;
a*(a-b)+(a-b)*b;
. ^^^^^^^ mul.2l;
a*(a-b)+b*(a-b);
^^^^^^^ muldiv.2l;
(a*a-a*b)+b*(a-b);
. ^^^^^^^ muldiv.2l;
(a*a-a*b)+(b*a-b*b);
^^^^^^^^^^^^^^^^^^^ sum.2l;
(b*a-b*b)+(a*a-a*b);
^^^^^^^^^^^^^^^^^^^ sub.3l;
a*a+((b*a-b*b)-a*b);
. ^^^^^^^^^^^^^ sub.7l;
a*a+(b*a-a*b-b*b);
. ^^^ mul.2l;
a*a+(a*b-a*b-b*b);
. ^^^^^^^ sub.2l;
a*a+(0-b*b);
^^^^^^^^^^^ sub.3l;
0+(a*a-b*b);
^^^^^^^^^^^ sum.2l;
(a*a-b*b)+0;
^^^^^^^^^^^ sum.3l;
};

0 comments on commit 9585374

Please sign in to comment.