Как убрать скобки в алгебраических выражениях с помощью Lean

Question

Я пытаюсь доказать одну алгебраическую теорему, используя Лин.Мой код

 import algebra.group
import algebra.ring
open algebra

variable {A : Type}

variables [s : ring A] (a b c : A)
include s

theorem clown (a b c d e : A) : 
(a + b  + e) * ( c + d) =   a * c + (b * c + e* c) + (a * d + b * d + e * d)   :=
calc

(a + b  + e) * ( c + d) = (a + (b + e))* (c +d)   : !add.assoc
                    ... = (a + (b + e)) * c + (a + (b + e)) * d   : by rewrite  left_distrib
                    ... =  a * c + (b + e) * c + (a + ( b + e)) * d : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a + (b + e)) * d : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + (b + e) * d) : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + (b * d + e * d) ) : by rewrite right_distrib
                    ... =  a * c + (b * c + e* c) + (a * d + b * d + e * d ) :  !add.assoc

 check clown

Пожалуйста, дайте мне знать, как убрать последнюю скобку.То есть я хочу получить только

a * c + b * c + e * c + a * d + b * d + e * d

Большое спасибо.

Answer 1

Возможное решение получается с использованием следующего кода

 import algebra.group
import algebra.ring
open algebra

variable {A : Type}

variables [s : ring A] (a b c : A)
include s

theorem clown (a b c d e : A)  : 
(a + b  + e) * ( c + d) =  a * c + a * d + b*c + b*d +e*c+e*d :=
calc

(a + b  + e) * ( c + d) = a*(c + d) + b*(c + d) + e*(c + d)   : by rewrite distrib_three_right
                   ...  = a * c + a * d + b*(c+d)+e*(c+d) : by rewrite *left_distrib
                   ...  = a * c + a* d + (b*c + b*d) +e*(c+d) : by rewrite *left_distrib
                   ... =  a * c + a* d + (b*c + b*d) +(e*c+e*d): by rewrite left_distrib
                   ... = a * c + a* d + b*c + b*d + (e*c+e*d) :  !add.assoc
                   ... = a * c + a* d + b*c + b*d + e*c+e*d :  !add.assoc

check clown

Другой пример

 import algebra.group
import algebra.ring
open algebra

variable {A : Type}

variables [s : ring A] (a b c : A)
include s

theorem clown (a b c d e f: A)  : 
(a + b  + e + f) * ( c + d) =  a * c + a * d + b*c + b*d +e*c+e*d  + f * c + f * d:=
calc

(a + b  + e + f) * ( c + d) = a*(c + d) + b*(c + d) + e*(c + d) + f*(c +d)  : by rewrite *right_distrib
                   ...  = a * c + a * d + b*(c+d)+e*(c+d) + f * (c + d): by rewrite *left_distrib
                   ...  = a * c + a* d + (b*c + b*d) +e*(c+d) + f*(c+d): by rewrite *left_distrib
                   ... =  a * c + a* d + (b*c + b*d) +(e*c+e*d)+ f*(c+d): by rewrite left_distrib
                   ... =  a * c + a* d + (b*c + b*d) +(e*c+e*d)+ (f*c+ f*d): by rewrite left_distrib
                   ... = a * c + a* d + b*c + b*d + (e*c+e*d)+ (f*c+f*d) :  !add.assoc
                   ... = a * c + a* d + b*c + b*d + e*c+e*d + (f*c + f*d):  !add.assoc
                   ... = a * c + a* d + b*c + b*d + e*c+e*d + f*c + f*d  :  !add.assoc

check clown

Тот же пример, но сокращенный

    variable {A : Type}

variables [s : ring A] 
include s

    theorem clown (a b c d e f: A)  : 
    (a + b  + e + f) * ( c + d) =  a * c + a * d + b*c + b*d +e*c+e*d  + f * c + f * d:=
    calc

    (a + b  + e + f) * ( c + d) = a*(c + d) + b*(c + d) + e*(c + d) + f*(c +d)  : by rewrite *right_distrib

                       ... =  a * c + a* d + (b*c + b*d) +(e*c+e*d)+ (f*c+ f*d): by rewrite *left_distrib

                       ... = a * c + a* d + b*c + b*d + e*c+e*d + f*c + f*d  :  by rewrite *add.assoc

    check clown

Другой пример

 import algebra.ring
open algebra
check mul_sub_left_distrib 
check add.assoc
variable {A : Type}

variables [s : ring A] 
include s

theorem clown (a b c d : A)  : 
    (a + b ) * ( c - d) =  a*c-a*d+ b*c- b*d:=
    calc

    (a + b) * ( c  -d) = a*(c-d) +b*(c-d) : by rewrite *right_distrib
                   ... = a*(c + -d) + b*(c-d) : rfl
                   ... = a*c  + a*-d+b*(c-d) : by rewrite left_distrib
                   ... = a*c + a*-d + (b*c - b*d): by rewrite mul_sub_left_distrib 
                   ... = a*c + a*-d + b*c - b*d : add.assoc
                   ... = a*c + -(a*d)+  b*c - b*d : by rewrite mul_neg_eq_neg_mul_symm
                   ... = a*c - a*d + b*c - b*d : rfl
 check clown  

Другой пример

import algebra.group
import algebra.ring
open algebra
variable {A : Type}

variables [s : ring A] 
include s

theorem clown (a b c d e : A)  : 
    (a + b + e ) * ( c - d) =  a*c -a*d + b*c - b*d + e*c - e*d:=
    calc
(a + b + e) * ( c - d) = a*(c-d) +b*(c-d) + e*(c-d) : by rewrite *right_distrib
                   ... = a*(c + -d) + b*(c+ -d) + e*(c-d): rfl
                   ... = a*c  + a*-d+(b*c +b*-d) + e*(c-d) : by rewrite *left_distrib
                   ... = a*c + a*-d + (b*c +b*-d)+ (e*c -e*d) : by rewrite *mul_sub_left_distrib 
                   ... = a*c + a*-d  + b*c + b*-d + (e*c - e*d) : !add.assoc
                   ... = a*c + a*-d + b*c + b*-d + e*c - e*d : !add.assoc
                   ... = a*c + -(a*d) + b*c +-(b*d) + e*c - e*d : by rewrite *mul_neg_eq_neg_mul_symm
                   ... = a*c - a*d + b*c - b*d + e*c - e*d : rfl
 check clown

Другой пример

import algebra.group
import algebra.ring
open algebra
variable {A : Type}

variables [s : ring A] 
include s

theorem clown (a b c d e f  : A)  : 
    (a + b + e + f) * ( c - d) =  a*c -a*d + b*c - b*d + e*c - e*d + f*c - f*d:=
    calc
(a + b + e + f) * ( c - d) = a*(c-d) +b*(c-d) + e*(c-d) + f*(c - d) : by rewrite *right_distrib
                   ... = a*(c + -d) + b*(c+ -d) + e*(c + -d) + f *(c-d): rfl
                   ... = a*c  + a*-d+(b*c +b*-d) + (e*c + e*-d)+ f*(c-d) : by rewrite *left_distrib
                   ... = a*c + a*-d + (b*c +b*-d)+ (e*c + e*-d) + (f*c - f*d) : by rewrite *mul_sub_left_distrib 
                   ... = a*c + a*-d  + b*c + b*-d + (e*c + e*-d) + (f*c -f*d): !add.assoc
                   ... = a*c + a*-d + b*c + b*-d + e*c + e*-d  + (f*c - f*d): !add.assoc
                   ... = a*c + a*-d + b*c + b*-d + e*c + e*-d  + f*c - f*d: !add.assoc
                   ... = a*c + -(a*d) + b*c +-(b*d) + e*c + - (e*d) + f*c - f*d : by rewrite *mul_neg_eq_neg_mul_symm
                   ... = a*c - a*d + b*c - b*d + e*c - e*d  + f*c - f*d : rfl
 check clown 

Другой пример

    import algebra.group
import algebra.ring
open algebra
variable {A : Type}

variables [s : ring A] 
include s

theorem clown (a b c d e f  : A)  : 
    (a + b - e  - f) * ( c - d) =  a*c -a*d + b*c -b*d -e*c + e*d - f*c + f*d :=
    calc
(a + b - e - f) * ( c - d) =(a + b + -e + -f)*(c-d) : rfl
                   ... = a*(c-d) +b*(c-d) + -e*(c-d) + -f*(c - d) : by rewrite *right_distrib
                   ... = a*(c + -d) + b*(c+ -d) + -e*(c + -d) + -f *(c-d): rfl
                   ... = a*c  + a*-d+(b*c +b*-d) + (-e*c + -e*-d)+ -f*(c-d) : by rewrite *left_distrib
                   ... = a*c + a*-d + (b*c +b*-d)+ (-e*c + -e*-d) + (-f*c - -f*d) : by rewrite *mul_sub_left_distrib 
                   ... = a*c + a*-d  + b*c + b*-d + (-e*c + -e*-d) + (-f*c - -f*d): !add.assoc
                   ... = a*c + a*-d + b*c + b*-d + -e*c + -e*-d  + (-f*c - -f*d): !add.assoc
                   ... = a*c + a*-d + b*c + b*-d + -e*c + -e*-d  + -f*c - -f*d: !add.assoc
                   ... = a*c + -(a*d) + b*c +-(b*d) + -e*c + - (-e*d) + -f*c - -f*d : by rewrite *mul_neg_eq_neg_mul_symm
                   ... = a*c - a*d + b*c -b*d + -e*c + - (-e*d) + -f*c  - -f*d : rfl
                   ... =a*c - a*d + b*c -b*d + -(e*c) + - -(e*d) + -(f*c)  - -(f*d) : by rewrite  *neg_mul_eq_neg_mul_symm
                   ... =a*c - a*d + b*c -b*d - e*c + - -(e*d) - f*c  - -(f*d) : rfl
                   ... = a*c - a*d + b*c -b*d - e*c + (e*d) - f*c  - -(f*d) : by rewrite neg_neg
                   ... = a*c - a*d + b*c -b*d - e*c + e*d - f*c +  - -(f*d) : rfl
                   ... = a*c - a*d + b*c -b*d - e*c + e*d - f*c +  (f*d) : by rewrite neg_neg
                   ... = a*c - a*d + b*c -b*d - e*c + e*d - f*c +  f*d : rfl

 check clown 

Answer 2

Если вы не против предположить, что ваше кольцо коммутативно, вы также можете использовать тактику ring.

import tactic.ring

variables {A : Type} [comm_ring A]

theorem clown (a b c d e : A) : 
  (a + b + e) * (c + d) = a * c + (b * c + e * c) + (a * d + b * d + e * d) :=
by ring

Answer 3

Это похоже на синтаксис Lean 2.Если вы специально не используете Lean 2 для режима теории гомотопического типа, я настоятельно рекомендую перейти на Lean 3, который выпускается с начала 2017 года.

По умолчанию операции + и * связаны слева.То есть a * c + b * c + e* c + a * d + b * d + e * d совпадает с (((((a * c + b * c) + e* c) + a * d) + b * d) + e * d).Вы можете доказать это окончательное равенство с помощью достаточного количества приложений add.assoc (переименовано add_assoc в Lean 3).В Lean 3 вы можете доказать это с помощью by simp или by simp only [add_assoc].