Module misc_

Fixes

Implicits refl_eqT [1].

Definition type_of := [T:Type; t:T]T.

Hints Resolve sym_eqT : sym.

Axioms

Proof irrelevance

Axiom proof_irrelevance : (P:Prop; x,y:P) x==y.

Axiom prop_uni : (A,B:Prop) (A->B) -> (B->A) -> A==B.

Extensionality

Axiom extensionality : (A:Type; T:A->Type; f,g:(x:A)(T x))
  ((x:A)(f x)==(g x)) -> f==g.

Lemma nondep_extensionality : (A,B:Type; f,g:A->B)
 ((x:A)(f x)==(g x)) -> f==g.
Proof.
 Intros A B; Apply extensionality with T:=[x:A]B.
Qed.
Hints Resolve nondep_extensionality.

Congruence


Theorem congr : (a,b:Type; f:a->b; u,v:a) (u == v) -> (f u) == (f v).
Proof.
Induction 1; Reflexivity.
Qed.

Theorem congr2 : (a,b,c:Type; f:a->b->c; u,v:a; s,t:b)
  u==v -> s==t -> (f u s) == (f v t).
Proof.
Intros; Case H; Case H0; Reflexivity.
Qed.

Plug




Very useful in the hints database!

Lemma plug : (X:Type; f:X->X; a,b:X)
  a==b -> (f a)==(f b).
Proof.
  NewDestruct 1; Reflexivity.
Qed.
Hints Resolve plug.

Lemma plug2 : (X:Type; f:X->X->X; a1,a2,b1,b2:X)
  a1==a2 -> b1==b2 -> (f a1 b1)==(f a2 b2).
Proof.
  NewDestruct 1; NewDestruct 1; Reflexivity.
Qed.
Hints Resolve plug2.

Lemma plug2_sx : (X,Y:Type; f:Y->X->X; a1,a2:Y; b1,b2:X)
  a1==a2 -> b1==b2 -> (f a1 b1)==(f a2 b2).
Proof.
  NewDestruct 1; NewDestruct 1; Reflexivity.
Qed.
Hints Resolve plug2_sx.

Lemma plug2_dx : (X,Y:Type; f:X->Y->X; a1,a2:X; b1,b2:Y)
  a1==a2 -> b1==b2 -> (f a1 b1)==(f a2 b2).
Proof.
  NewDestruct 1; NewDestruct 1; Reflexivity.
Qed.
Hints Resolve plug2_dx.

Natural map from Type to Prop.


Inductive prop_of_type [A:Type] : Prop :=
 | prop_of_type_intro : (x:A) (prop_of_type A).

Hints Resolve prop_of_type_intro.

Non empty types.

Inductive non_empty [A:Type] : Type :=
 | non_empty_intro : (x:A) (non_empty A).
  


Types with a sigle elements.

Record is_singleton [A:Type] : Type := {
  is_singleton_exists : (non_empty A);
  is_singleton_unique : (x,y:A) x==y
 }.

Set_Of

Inductive Set_Of [A:Type; P:A->Prop] : Type :=
 | set_of_intro : (x:A)(P x) -> (Set_Of P).

Definition forget [A:Type; P:A->Prop; x:(Set_Of P)] : A.
Proof.
  NewDestruct 1; Assumption.
Defined.

JMeq

Definition of JMeq

Inductive JMeq [A: Type; a:A] : (B: Type; b:B) Prop :=
 | JMeq_refl : (JMeq a a).

Infix 9 "-=-" JMeq.

Lemma JMeq_sym : (A,B: Type; a:A; b:B)(a -=- b) -> (b -=- a).
Proof.
  NewDestruct 1; Split.
Qed.

Lemma JMeq_trs : (A,B,C: Type; a:A; b:B; c:C)
  (a -=- b) -> (b -=- c) -> (a -=- c).
Proof.
  NewDestruct 1; NewDestruct 1; Split.
Qed.

Lemma eqT_JMeq : (A:Type; a,b: A) (a == b) -> (a -=- b).
Proof.
  NewDestruct 1; Split.
Qed.

Theorem JMeq_type_eqT : (A,B:Type; a:A; b:B)
  (a -=- b) -> A==B.
Proof.
  NewDestruct 1; Split.
Qed.

Transport and JMeq_eqT


Definition transport [A,B:Type; e:A==B; a:A] : B.
Proof.
  NewDestruct 1; Intro a; Exact a.
Defined.

Lemma eqT_rect_simpl : (A:Type; x:A; P:A->Type; f:(P x); H:x==x)
  (eqT_rect A x [y:A](P y) f x H)==f.
Proof.
  Intros.
  Assert H==(refl_eqT x).
  Apply proof_irrelevance.
  Rewrite H0; Split.
Qed.

Lemma JMeq_transport_eqT : (A,B:Type; a:A; b:B; H:(a-=-b); HT:A==B)
 (transport HT a)==b.
Proof.
  Intros.
  LetTac P := [X:Type; x:X] (E:X==B)(transport E x)==b.
  Cut (P A a).
  Auto.
  Elim (JMeq_sym H); Unfold P; Intros.
  Assert e:(refl_eqT B)==E.
  Apply proof_irrelevance.
  NewDestruct e; Split.
Qed.

Theorem JMeq_eqT : (A:Type; a,b:A) (a-=-b) -> a==b.
Proof.
  Intros.
  Transitivity (transport (refl_eqT A) a).
  Split.
  Apply JMeq_transport_eqT.
  Assumption.
Qed.

Lemma transport_refl : (A:Type; H:A==A; x:A) (transport H x)==x.
Proof.
  Intros; Assert e : (refl_eqT ?)==H.
  Apply proof_irrelevance; Split.
  NewDestruct e; Split.
Qed.

Lemma transport_eq : (A,B:Type; H1,H2:A==B; x:A)
  (transport H1 x)==(transport H2 x).
Proof.
  Intros.
  Assert H1==H2.
  Apply proof_irrelevance.
  Rewrite H; Split.
Qed.

End Misc_.