Library firstorder

Quantifiers

In this file, we simulate first-order logic within the richer setting of Coq's logic. To this effect we declare a type T for terms, a unary predicate P, a proposition Q, and a relation R.

We then use the tactics intro and apply to reason about universal quantifications, and exists and destruct for existential quantifications.

Variable T : Type.
Variable P : T -> Prop.
Variable Q : Prop.
Variable R : T -> T -> Prop.

Goal (exists x:T , forall y:T, R x y)
  -> (forall y:T, exists x:T , R x y).
Proof.
  intros H y.
  destruct H.
  exists x.
  apply H.
Qed.

Goal (exists x:T , P x \/ Q) -> ((exists x:T , P x ) \/ Q).
Proof.
  intros. destruct H. destruct H.
  + left. exists x. exact H.
  + right. exact H.
Qed.

For the next result, we need to be able to introduce an existential with an arbitrary term. This is not allowed in Coq, where types may be empty. We thus postulate the existence of at least one element in T.

Variable a : T.

Goal ((exists x:T , P x ) \/ Q) -> (exists x:T , P x \/ Q).
Proof.
admit.
Qed.

Equality

Variable f : T -> T.

Goal forall x y : T, x = y -> f x = f y.
Proof.
  intros x y Heq.
  rewrite Heq.
  reflexivity.
Qed.

Goal forall x y : T, x = y -> P y -> P x.
Proof.
  intros x y Heq H.
  rewrite Heq.
  exact H.
Qed.

Goal forall x y : T, forall z:T,
  x = y -> f y = z -> P (f x) -> P z.
Proof.
  intros x y z Hxy Hfyz H.
  rewrite<- Hxy in Hfyz.
  rewrite Hfyz in H.
  exact H.
Qed.

Symmetry and transitivity are consequences of the substitution principle embodied by the rewrite tactic: prove it!

Lemma symmetry : forall x y : T, x = y -> y = x.
Proof.
admit.
Qed.

Lemma transitivity : forall x y z : T, x = y -> y = z -> x = z.
Proof.
admit.
Qed.

Functions

Here we define a new sort of terms, and various properties of functions over it. Prove the theorem as an exercise.

Module Functions.

  Variable A : Type.

  Definition injective (f:A->A) :=
    forall x:A, forall y:A, f x = f y -> x = y.

  Definition surjective (f:A->A) :=
    forall x:A, exists y:A , x = f y.

  Definition bijective (f:A->A) := injective f /\ surjective f.

  Definition involutive (f:A->A) := forall x:A, f (f x) = x.

  Theorem inv_bij : forall (f:A->A), involutive f -> bijective f.
  Proof.
    admit.
  Qed.

End Functions.

Drinker's paradox

As an advanced exercise (probably for next time) prove that the drinker's formula holds, using classical reasoning and assuming that the universe of terms is not empty.

Module Drinker.

Assume a non-empty bar, and a predicate indicating which persons in the bar drink.

  Variable Person : Type.
  Variable p : Person.
  Variable Drinks : Person -> Prop.

You can use any of the two equivalent axioms. You probably want to use LEM first, then try using only RAA for added difficulty.

  Axiom RAA : forall P:Prop, ~~P -> P.
  Axiom LEM : forall P:Prop, P \/ ~P.

  Goal exists x:Person , Drinks x -> forall y:Person, Drinks y.
  Proof.
    admit.
  Qed.

End Drinker.