Some proofs in predicate calculus

Consider the following declarations :

 Section A_declared.
 Variables (A : Set )
           (P Q : A->Prop)
           (R : A->A->Prop).

Prove the following theorems:

 (forall a b:A, R a b) -> forall a b:A, R b a

 (forall a:A, P a -> Q a) -> (forall a:A, P a) -> forall a:A, Q a

 (forall a b:A, R a b) -> forall a:A, R a a

Solution

Look at this file

Note

Each of these proofs can be replaced by a simple call to auto.

Going home

Pierre Castéran