Quelle bug_4198.v Sprache: Coq

(* Check that the subterms of the predicate of a match are taken into account *)

Require Import TestSuite.list.

Goal forall A (x x' : A) (xs xs' : list A) (H : cons x xs = cons x' xs'),
       let k :=
           (match H in (_ = y) return x = hd x y with
              | eq_refl => eq_refl
            end : x = x')
       in k = k.
  simpl.
  intros.
  match goal with
    | [ |- context G[@hd] ] => idtac
  end.
Abort.

(* This second example comes from CFGV where inspecting subterms of a
   match is expecting to inspect first the term to match (even though
   it would certainly be better to provide a "match x with _ end"
   construct for generically matching a "match") *)

Ltac find_head_of_head_match T :=
  match T with context [?E] =>
    match T with
    | E => fail 1
    | _ => constr:(E)
    end
  end.

Ltac mydestruct :=
  match goal with
  | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E
  end.

Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
intros.
mydestruct.
Abort.

quality97%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

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.