Require Import ssreflect.
Variable term:Type.
(* Declaring constant symbol and function symbol of arity 2 *)
Variable a:term.
Variable f:term->term->term.
(* Check that terms are well-formed *)
Check f a a.
(* Declaring predicate symbols, and a propositional variable
(predicate symbol of arity 0) *)
Variables F: term->Prop.
Variables Rel: term->term->Prop.
Variables G: Prop.
(* PREDICATE LOGIC *)
(* A small example of how to use the forall quantifier. *)
Theorem fa: forall n m, (forall p, Rel p m) -> Rel n m.
Proof.
move => n.
move => m.
move => h.
apply:h.
Qed.
Theorem b: (forall m, G -> F m) -> G -> forall n, F n.
Proof.
move => h.
move => g.
move => n.
apply:h.
done.
Qed.
Theorem c: (forall m, F m) -> F (f a a).
Proof.
move => h.
apply:h.
Qed.
(* A small example of how to use the exists quantifier. *)
Theorem ex: forall n, (exists m, F n /\ Rel n m) -> exists p,Rel n p.
Proof.
move => n h1.
(* at this point, I would like to say that p should be m,
but m is just a quantified variable at this point,
so I use a case to destroy the existential quantifier in h1 *)
case:h1 => m h2.
(* at this point, I really want to say that p should be m,
this is done with exists *)
exists m.
(* The rest is easy: finish it as an exercise *)
case:h2.
done.
Qed.
Theorem d: F (f a a) -> exists n, F n.
Proof.
move => h.
exists (f a a).
done.
Qed.
Theorem a': (exists n, F n) -> (forall m, F m->G) -> G.
Proof.
move => h.
move => h1.
case:h.
done.
Qed.
(* PROVING EQUALITY *)
Theorem Eq1: forall x:term, x=x.
Proof.
done.
Qed.
(* USING EQUALITY *)
Theorem Eq_f1: forall x1 x1' x2:term, x1=x1'->f x1 x2 = f x1' x2.
Proof.
move => x1 x1' x2 h.
rewrite h.
done.
Qed.
Theorem Eq_f2: forall x1 x2 x2':term, x2=x2'->f x1 x2 = f x1 x2'.
Proof.
move => x1.
move => x2.
move => x2'.
move => h.
rewrite h.
done.
Qed.
Theorem Eq_F: forall x1 x1':term, x1=x1' -> F x1' -> F x1.
Proof.
move => x1.
move => x1'.
move => h.
rewrite h.
done.
Qed.
Theorem Eq_sym: forall x1 x1':term, x1=x1' -> x1'=x1.
Proof.
move => x1.
move => x1'.
move => h.
rewrite h.
done.
Qed.
Theorem Eq_trans: forall x1 x1' x1'':term, x1=x1' -> x1'=x1'' -> x1=x1''.
Proof.
move => x1.
move => x1'.
move => x1''.
move => h1.
move => h2.
rewrite h1.
rewrite h2.
done.
Qed.
Theorem Eq_Fback: forall x1 x1':term, x1=x1' -> F x1 -> F x1'.
Proof.
move => x1.
move => x1'.
move => h.
move => h1.
rewrite -h.
done.
Qed.