Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: change.v Sprache: Coq

Original von: Coq^©

(* A few tests of the syntax of clauses and of the interpretation of change *)

Goal let a := 0+0 in a=a.
intro.
change 0 in (value of a).
change ((fun A:Type => A) nat) in (type of a).
Abort.

Goal forall x, 2 + S x = 1 + S x.
intro.
change (?u + S x) with (S (u + x)).
Abort.

(* Check the combination of at, with and in (see bug #2146) *)

Goal 3=3 -> 3=3. intro H.
change 3 at 2 with (1+2).
change 3 at 2 with (1+2) in H |-.
change 3 with (1+2) in H at 1 |- * at 1.
(* Now check that there are no more 3's *)
change 3 with (1+2) in * || reflexivity.
Qed.

(* Note: the following is invalid and must fail
change 3 at 1 with (1+2) at 3.
change 3 at 1 with (1+2) in *.
change 3 at 1 with (1+2) in H at 2 |-.
change 3 at 1 with (1+2) at 3.
change 3 at 1 with (1+2) in H |- *.
change 3 at 1 with (1+2) in H, H|-.
change 3 at 1.
*)

(* Test that pretyping checks allowed elimination sorts *)

Goal True.
Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
Fail change True with
match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
Abort.

(* Check absence of loop in identity substitution (was failing up to
Sep 2014, see #3641) *)

Goal True.
change ?x with x.
Abort.

(* Check typability after change of type subterms *)
Goal nat = nat :> Set.
Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
Abort.

(* Check typing env for rhs is the correct one *)

Goal forall n, let x := n in id (fun n => n + x) 0 = 0.
intros.
unfold x.
(* check that n in 0+n is not interpreted as the n from "fun n" *)
change n with (0+n).
Abort.

(* Check non-collision of non-normalized defined evars with pattern variables *)

Goal exists x, 1=1 -> x=1/\x=1.
eexists ?[n]; intros; split.
eassumption.
match goal with |- ?x=1 => change (x=1) with (0+x=1) end.
match goal with |- 0+1=1 => trivial end.
Qed.

(* Mini-check that no_check does not check *)

Goal True -> False.
intro H.
change_no_check nat.
apply S.
change_no_check nat with bool.
change_no_check nat in H.
change_no_check nat with (bool->bool) in H.
exact (H true).
Fail Qed.
Abort.

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