Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: tarski_query.pvs Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** John Major's Equality as proposed by Conor McBride

  Reference:

  [McBride] Elimination with a Motive, Proceedings of TYPES 2000,
  LNCS 2277, pp 197-216, 2002.

*)

Set Implicit Arguments.

Unset Elimination Schemes.

Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
    JMeq_refl : JMeq x x.

Set Elimination Schemes.

Arguments JMeq_refl {A x} , [A] x.

Register JMeq as core.JMeq.type.
Register JMeq_refl as core.JMeq.refl.

Hint Resolve JMeq_refl : core.

Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.

Register JMeq_hom as core.JMeq.hom.

Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
Proof.
intros; destruct H; trivial.
Qed.

Hint Immediate JMeq_sym : core.

Register JMeq_sym as core.JMeq.sym.

Lemma JMeq_trans :
forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
Proof.
destruct 2; trivial.
Qed.

Register JMeq_trans as core.JMeq.trans.

Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.

Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
  P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Register JMeq_ind as core.JMeq.ind.

Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
  P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
  P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
   P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
   P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
   P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_congr :
forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
Proof.
intros A x B f y H; case JMeq_eq with (1 := H); trivial.
Qed.

Register JMeq_congr as core.JMeq.congr.

(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)

Require Import Eqdep.

Lemma JMeq_eq_dep_id :
forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
Proof.
destruct 1.
apply eq_dep_intro.
Qed.

Lemma eq_dep_id_JMeq :
forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
Proof.
destruct 1.
apply JMeq_refl.
Qed.

(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *)

Lemma eq_dep_JMeq :
forall U P p x q y, eq_dep U P p x q y -> JMeq x y.
Proof.
destruct 1.
apply JMeq_refl.
Qed.

Lemma eq_dep_strictly_stronger_JMeq :
exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y.
Proof.
exists bool. exists (fun _ => True). exists true. exists false.
exists I. exists I.
split.
- trivial.
- intro H.
  assert (true=false) by (destruct H; reflexivity).
  discriminate.
Qed.

(** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
    is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)

Lemma JMeq_eq_dep :
  forall U (P:U->Type) p q (x:P p) (y:P q),
  p = q -> JMeq x y -> eq_dep U P p x q y.
Proof.
intros.
destruct H.
apply JMeq_eq in H0 as ->.
reflexivity.
Qed.

(* Compatibility *)
Notation sym_JMeq := JMeq_sym (only parsing).
Notation trans_JMeq := JMeq_trans (only parsing).

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.