>PhoX> Sort term. Sort term defined >PhoX> Cst f : term term. f : term term >PhoX> Cst zero : term. zero : term >PhoX> def Im A y = x (A x f x = y). Im = \A,y x:A f x = y : (term prop) term prop >PhoX> def ker x = f x = zero. ker = \x (f x = zero) : term prop >PhoX> def inclus A B = x (A x B x). inclus = \A,B x:A B x : ('a prop) ('a prop) prop >PhoX> Cst plus : term term term. plus : term term term >PhoX> Cst moins : term term term. moins : term term term >PhoX> def Plus A B x = y,z (A y B z x = (plus y z)). Plus = \A,B,x y,z (A y B z x = plus y z) : (term prop) (term prop) term prop >PhoX> (* On a supposé, implicitement, que les ensembles de termes sont des espaces vectoriels et que f est une application linéaire. Les lemmes ci-dessous expriment les propriétés des espaces vectoriels (resp. des applications linéaires) dont on a besoin dans la preuve faite. Ils pourraient être prouvés sans difficulté à partir des axiomes d'espace vectoriel et de la définition d'une application linéaire. On a préféré ici se concentrer sur l'essentiel et on les admettra donc*) >PhoX> claim lemme1 x,y (f x = f y ker (moins y x)). lemme1 = x,y (f x = f y ker (moins y x)) : theorem >PhoX> claim lemme2 x,y,z plus x (plus z (moins y x))=plus y z. lemme2 = x,y,z plus x (plus z (moins y x)) = plus y z : theorem >PhoX> claim lemme3 x,y (ker x ker y ker (plus x y)). lemme3 = x,y (ker x ker y ker (plus x y)) : theorem >PhoX> claim lemme4 y,a,b (plus a b = y ker b f a = f y). lemme4 = y,a,b (plus a b = y ker b f a = f y) : theorem >PhoX> claim lemme5 A,B a (A a Plus A B a). lemme5 = A,B a:A Plus A B a : theorem >PhoX> goal A,B ((inclus (Im A) (Im B)) (inclus (Plus A ker) (Plus B ker))). Here is the goal: goal 1/1 A,B (inclus (Im A) (Im B) inclus (Plus A ker) (Plus B ker)) %PhoX% intro 6. 2 goals created. goal 2/2 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x Plus B ker x %PhoX% elim H0. 1 goal created. goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z (A y ker z x = plus y z) Plus B ker x %PhoX% elim H1. 1 goal created. goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H2 := A y ker z x = plus y z Plus B ker x %PhoX% lefts H2. 1 goal created. goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Plus B ker x %PhoX% use Im B (f y). 2 goals created. goal 2/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) Plus B ker x %PhoX% elim G. 1 goal created. goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 f x0 = f y Plus B ker x %PhoX% intro 2. 1 goal created. goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 f x0 = f y B ?1 ker ?2 x = plus ?1 ?2 %PhoX% instance ?1 x0. Here are the goals: goal 3/3 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 2/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 f x0 = f y B x0 ker ?2 x = plus x0 ?2 %PhoX% instance ?2 plus z (moins y x0). Here are the goals: goal 3/3 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 2/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 f x0 = f y B x0 ker (plus z (moins y x0)) x = plus x0 (plus z (moins y x0)) %PhoX% left H5. 1 goal created. goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y B x0 ker (plus z (moins y x0)) x = plus x0 (plus z (moins y x0)) %PhoX% intros. 3 goals created. goal 3/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y x = plus x0 (plus z (moins y x0)) goal 2/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y ker (plus z (moins y x0)) goal 1/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y B x0 %PhoX% axiom H5. 0 goal created. goal 4/4 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 3/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 2/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y x = plus x0 (plus z (moins y x0)) goal 1/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y ker (plus z (moins y x0)) %PhoX% use ker (moins y x0). 2 goals created. goal 2/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y ker (moins y x0) goal 1/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := ker (moins y x0) ker (plus z (moins y x0)) %PhoX% elim lemme3. 1 goal created. goal 1/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := ker (moins y x0) ker z ker (moins y x0) %PhoX% intro. 2 goals created. goal 2/6 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := ker (moins y x0) ker (moins y x0) goal 1/6 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := ker (moins y x0) ker z %PhoX% axiom H4. 0 goal created. goal 5/5 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 4/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 3/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y x = plus x0 (plus z (moins y x0)) goal 2/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y ker (moins y x0) goal 1/5 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := ker (moins y x0) ker (moins y x0) %PhoX% axiom G0. 0 goal created. goal 4/4 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 3/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 2/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y x = plus x0 (plus z (moins y x0)) goal 1/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y ker (moins y x0) %PhoX% elim lemme1. 1 goal created. goal 1/4 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y f x0 = f y %PhoX% axiom H6. 0 goal created. goal 3/3 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 2/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y x = plus x0 (plus z (moins y x0)) %PhoX% apply -1 x0 -2 y -3 z lemme2. 1 goal created. goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z G := Im B (f y) H5 := B x0 H6 := f x0 = f y G0 := plus x0 (plus z (moins y x0)) = plus y z x = plus x0 (plus z (moins y x0)) %PhoX% intro. 0 goal created. goal 2/2 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im B (f y) %PhoX% elim H. 1 goal created. goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z Im A (f y) %PhoX% intro. 1 goal created. goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z A ?3 f ?3 = f y %PhoX% intro. 2 goals created. goal 2/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z f ?3 = f y goal 1/3 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z A ?3 %PhoX% axiom H2. 0 goal created. goal 2/2 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x goal 1/2 H := inclus (Im A) (Im B) H0 := Plus A ker x H1 := z0 (A y ker z0 x = plus y z0) H3 := x = plus y z H2 := A y H4 := ker z f y = f y %PhoX% intro. 0 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := Im A x Im B x %PhoX% left H0. 1 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 f x0 = x Im B x %PhoX% left H0. 1 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x Im B x %PhoX% use Plus B ker x0. 2 goals created. goal 2/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x Plus B ker x0 goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x G := Plus B ker x0 Im B x %PhoX% left G. 1 goal created. goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H2 := z (B x1 ker z x0 = plus x1 z) Im B x %PhoX% lefts H2. 1 goal created. goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H2 := B x1 ker z x0 = plus x1 z Im B x %PhoX% lefts H2. 1 goal created. goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z Im B x %PhoX% intro . 1 goal created. goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z B ?4 f ?4 = x %PhoX% intro. 2 goals created. goal 2/3 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z f ?4 = x goal 1/3 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z B ?4 %PhoX% axiom H2. 0 goal created. goal 2/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x Plus B ker x0 goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z f x1 = x %PhoX% apply -4 H3 -5 H4 lemme4. 1 goal created. goal 1/2 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x H3 := x0 = plus x1 z H2 := B x1 H4 := ker z G := f x1 = f (plus x1 z) f x1 = x %PhoX% intro. 0 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x Plus B ker x0 %PhoX% elim H. 1 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x Plus A ker x0 %PhoX% elim lemme5. 1 goal created. goal 1/1 H := inclus (Plus A ker) (Plus B ker) H0 := A x0 H1 := f x0 = x A x0 %PhoX% axiom H0. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = A,B (inclus (Im A) (Im B) inclus (Plus A ker) (Plus B ker)) : theorem bye