Quelle bug_3699.v Sprache: Coq

Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *)
(* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Inductive trunc_index := minus_two | trunc_S (_ : trunc_index).
Axiom IsTrunc : trunc_index -> Type -> Type.
Existing Class IsTrunc.
Axiom Contr : Type -> Type.
Inductive Trunc (n : trunc_index) (A :Type) : Type := tr : A -> Trunc n A.
Module NonPrim.
  Unset Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) : fibration_scope.
  Notation "x .2" := (pr2 x) : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End NonPrim.

Module Prim.
  Set Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) : fibration_scope.
  Notation "x .2" := (pr2 x) : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End Prim.

quality99%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.