Grammar vernac vernac := rlemma_cmd [ "RLemma" command:command($a) ":" command:command($b) "." ] -> [ <:vernac:> ]. Grammar vernac vernac := property_cmd [ "Property" command:command($a) ":=" command:command($b) "." ] -> [<:vernac:> ]. Grammar vernac vernac := outremark_cmd [ "OutRemark" command:command($a) ":" command:command($b) "." ] -> [<:vernac:> ]. Parameter G : Type. Parameter EQ : G-> G-> Prop. Axiom EQ_refl : (a: G) (EQ A A). Axiom EQ_symmA : (a,b: G) (EQ a b) -> (EQ b a). Lemma EQ_symm : (a,b: G) (EQ a b) -> (EQ b a). Proof EQ_symmA. Axiom EQ_transA : (a,b,c: G) (EQ a b) -> (EQ b c) -> (EQ a c). Lemma EQ_trans : (a,b,c: G) (EQ a b) -> (EQ b c) -> (EQ a c). Proof EQ_transA. Parameter AND : Prop -> Prop -> Prop. Axiom AND_conj : (P,Q: Prop) P -> Q -> (AND P Q). Axiom AND_proj1 : (P,Q: Prop) (AND P Q) -> P. Axiom AND_proj2 : (P,Q: Prop) (AND P Q) -> Q. Definition Look_at := [A: G]TRUE. Definition Just_look_at := True1. (**** here are some other similar things not used in the example ***) (**** but which might be useful for developing further *****) Definition Apply0 := [P: Prop] P. Definition Apply1 := [P: G -> Prop][X: G](P X). Definition Apply2 := [P: G-> G -> Prop][X, Y: G](P X Y). Definition Apply3 := [P: G-> G -> G -> Prop][X,Y,Z: G](P X Y Z). Definition TRUE := (P: Prop) P -> P. Definition True0 := [P: Prop][p:P]p. Definition True1 := [X: G]True0. Definition True2 := [X,Y: G]True0. Definition Try_conclude := [P: Prop]P -> P. Definition Triv := [P: Prop][p: P] p. Definition Consider0 := [P: Prop]TRUE. Definition Consider1 := [P: G -> Prop]TRUE. Definition Consider2 := [P: G->Ens->Prop]TRUE. Definition Just_consider0 := [P: Prop]True0. Definition Just_consider1 := [P: G -> Prop]True0. Definition Just_consider2 := [P: G->G->Prop]True0. Property Imply := [P,Q: Prop](Apply0 P) -> (Apply0 Q). Lemma apply_Imply : (P, Q : Prop)( Imply P Q ) -> ( Apply0 P ) -> ( Apply0 Q ). Proof [P, Q : Prop][ hyp : ( Imply P Q )] [ h00001 : ( Apply0 P )] ( hyp h00001 ). (********** finished with basic stuff *******) (********** the example starts here ********) Parameter mult : G-> G -> G. RLemma assoc : (x,y,z: G)(Look_at (mult x (mult y z))) -> (EQ (mult x (mult y z)) (mult (mult x y) z)). RLemma assoc_look : (x,y,z: G)(Look_at (mult x (mult y z))) -> (Look_at (mult (mult x y) z)). RLemma look_mult_1 : (a,b: G) (Look_at (mult a b))-> (Look_at a). RLemma look_mult_2 : (a,b: G) (Look_at (mult a b)) -> (Look_at b). RLemma subst_1 : (a,b,u : G) (Look_at (mult a b))-> (EQ u a) -> (EQ (mult u b) (mult a b)). RLemma look_subst_1 : (a,b,u : G) (Look_at (mult a b))-> (EQ u a) -> (Look_at (mult u b)). RLemma subst_2 : (a,b,u : G) (Look_at (mult a b))-> (EQ u b) -> (EQ (mult a u) (mult a b)). RLemma look_subst_2 : (a,b,u : G) (Look_at (mult a b))-> (EQ u b) -> (Look_at (mult a u)). (**** in what is below, I have erased the steps which are not used (but you ***** can see how many there were from the numbering ) ************) Section testA. Variables a,b,z: G. Hypothesis l : (Look_at (mult a (mult b (mult a b)))). Hypothesis p : (EQ z (mult a (mult b (mult a b)))). (***************** one iteration *******************) Remark automatic_00002 : (EQ ( mult a ( mult b ( mult a b ) ) ) ( mult ( mult a b ) ( mult a b ) ) ). Proof ( assoc a b ( mult a b ) l ). Remark automatic_00003 : (Look_at ( mult ( mult a b ) ( mult a b ) ) ). Proof ( assoc_look a b ( mult a b ) l ). (***************** one iteration *******************) Remark automatic_00008 : (EQ z ( mult ( mult a b ) ( mult a b ) ) ). Proof ( EQ_trans z ( mult a ( mult b ( mult a b ) ) ) ( mult ( mult a b ) ( mult a b ) ) p automatic_00002 ). Remark automatic_00010 : (EQ ( mult ( mult a b ) ( mult a b ) ) ( mult ( mult ( mult a b ) a ) b ) ). Proof ( assoc ( mult a b ) a b automatic_00003 ). (***************** one iteration *******************) Remark automatic_00024 : (EQ z ( mult ( mult ( mult a b ) a ) b ) ). Proof ( EQ_trans z ( mult ( mult a b ) ( mult a b ) ) ( mult ( mult ( mult a b ) a ) b ) automatic_00008 automatic_00010 ). (**** the next thing is added by the user ******) OutRemark conclusion : (EQ z ( mult ( mult ( mult a b ) a ) b ) ). Proof automatic_00024. (****** now we apply the widget5 command e to end the section ******) (**** this doesnt provide anything interesting but shows how e works ****) End testA. Lemma test : (a, b, z : G)( Look_at ( mult a ( mult b ( mult a b ) ) ) ) -> ( EQ z ( mult a ( mult b ( mult a b ) ) ) ) -> ( EQ z ( mult ( mult ( mult a b ) a ) b ) ). Proof [a, b, z : G][l : ( Look_at ( mult a ( mult b ( mult a b ) ) ) )] [p : ( EQ z ( mult a ( mult b ( mult a b ) ) ) )] (conclusion a b z l p).