Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_5149.v Sprache: Coq

Original von: Coq^©

Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
intros.
eexists.
rewrite <- H.
eassumption.
Qed.

Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type)
            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 :
flat_type -> Type)
            (v v' : interp_flat_type1 t'),
    v = v' ->
    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 ->
interp_flat_type0 t0)
           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
           (x' : interp_flat_type1 (Tbase t)) (T : Type)
           (flatten_binding_list : forall t0 : flat_type,
               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
           (s : forall x0 : base_type_code, prod (exprf (Tbase x0))
(interp_flat_type1 (Tbase x0)) -> T)
           (pair : forall A B : Type, A -> B -> prod A B),
      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
        (flatten_binding_list t' (SmartVarVar t' v') v) ->
      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1
t'0)
              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0
x'0))
            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf
(Tbase t0) x0 = x'0) ->
      interpf (Tbase t) x = x'.
Proof.
  intros ?????????????????????? interpf_SmartVarVar.
  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail
"too early".
  Undo.
  (** Implicitly at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
  solve [eapply interpf_SmartVarVar; subst; eassumption].
  Undo.
  Unset Solve Unification Constraints.
  (* User control of when constraints are solved *)
  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
Qed.

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