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.