Library Mtac2.lib.Logic

Set Implicit Arguments.

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.

Reserved Notation "x =m= y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x =m= y" (at level 70, no associativity).

First-order quantifiers

ex P, or simply exists x, P x, or also exists x:A, P x, expresses the existence of an x of some type A in Set which satisfies the predicate P. This is existential quantification.

ex2 P Q, or simply exists2 x, P x & Q x, or also exists2 x:A, P x & Q x, expresses the existence of an x of type A which satisfies both predicates P and Q.

Universal quantification is primitively written forall x:A, Q. By symmetry with existential quantification, the construction all P is provided too.

Inductive mex (A:Type) (P:A -> Prop) : Prop :=
mex_intro : forall x:A, P x -> mex (A:=A) P.

Equality

eq x y, or simply x=y expresses the equality of x and y. Both x and y must belong to the same type A. The definition is inductive and states the reflexivity of the equality. The others properties (symmetry, transitivity, replacement of equals by equals) are proved below. The type of x and y can be made explicit using the notation x = y :> A. This is Leibniz equality as it expresses that x and y are equal iff every property on A which is true of x is also true of y

Inductive meq (A:Type) (x:A) : A -> Prop :=
     meq_refl : x =m = x :>A
where "x =m= y :> A" := (@meq A x y) : type_scope.

Notation "x =m= y" := (x =m = y :>_) : type_scope.

Arguments meq {A} x _.
Arguments meq_refl {A x} , [A] x.

Arguments meq_ind [A] x P _ y _.
Arguments meq_rec [A] x P _ y _.
Arguments meq_rect [A] x P _ y _.

Section equality.
  Variables A : Type.
  Variables x y z : A.

  Theorem meq_sym : x =m = y -> y =m = x.
  Proof.
    destruct 1; reflexivity.
  Defined.

  Theorem meq_trans : x =m = y -> y =m = z -> x =m = z.
  Proof.
    destruct 2; trivial.
  Defined.

  Variable B : Type.
  Variable f : A -> B.
  Theorem mf_equal : x =m = y -> f x =m = f y.
  Proof.
    destruct 1; reflexivity.
  Defined.
End equality.

  Definition meq_ind_r :
    forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y =m = x -> P y.
    intros A x P H y H0. elim meq_sym with (1 := H0); assumption.
  Defined.

  Definition meq_rec_r :
    forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y =m = x -> P y.
    intros A x P H y H0; elim meq_sym with (1 := H0); assumption.
  Defined.

  Definition meq_rect_r :
    forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y =m = x -> P y.
    intros A x P H y H0; elim meq_sym with (1 := H0); assumption.
  Defined.