Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_4644.v Sprache: Coq

Original von: Coq^©

(* Testing a regression of unification in 8.5 in problems of the form
   "match ?y with ... end = ?x args" *)

Lemma foo : exists b, forall a, match a with tt => tt end = b a.
Proof.
eexists. intro.
refine (_ : _ = match _ with tt => _ end).
refine eq_refl.
Qed.

(**********************************************************************)

Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
Require Export Coq.Classes.Morphisms.
Require Import Coq.Lists.List.

Global Set Implicit Arguments.

Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs))
           ls
  : P ls
  := match ls with
     | nil => N
     | x::xs => C x xs
     end.

Axiom list_caset_Proper'
  : forall {A P},
    Proper (eq
              ==> pointwise_relation _ (pointwise_relation _ eq)
              ==> eq
              ==> eq)
           (@list_caset A (fun _ => P)).
Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool),
        match a3 with
        | nil => 0
        | (_ :: _)%list => 1
        end = y2 a4.
  clear; eexists; intros.
  reflexivity. Undo.
  Local Ltac t :=
    lazymatch goal with
    | [ |- match ?v with nil => ?N | cons x xs => @?C x xs end = _ :> ?P ]
      => let T := type of v in
         let A := match (eval hnf in T) with list ?A => A end in
         refine (@list_caset_Proper' A P _ _ _ _ _ _ _ _ _
                 : @list_caset A (fun _ => P) N C v = match _ with nil => _ | cons x xs => _ end)
    end.
  (etransitivity; [ t | reflexivity ]) || fail 0 "too early".
  Undo.
  t.
Abort.

¤ Dauer der Verarbeitung: 0.13 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.