Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: cc.v Sprache: Coq

Original von: Coq^©

Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a.
intros.
congruence.
Qed.

Theorem t2 :
forall (A : Set) (a b : A) (f : A -> A) (g : A -> A -> A),
a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a.
intros.
congruence.
Qed.

(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)

Theorem t3 :
forall (N : Set) (o : N) (s d : N -> N),
s (s (s (s (s (s (s (s (s (s (s (s (s (s (s o)))))))))))))) = o ->
s (s (s (s (s (s (s (s (s (s o))))))))) = o ->
s (s (s (s (s (s o))))) = o -> o = s o.
intros.
congruence.
Qed.

(* Examples that fail due to dependencies *)

(* yields transitivity problem *)

Theorem dep :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x)
   (x y : A) (e : x = y) (e0 : f y = g y), f x = g x.
intros;  dependent rewrite e; exact e0.
Qed.

(* yields congruence problem *)

Theorem dep2 :
forall (A B : Set)
   (f : forall (A : Set) (b : bool), if b then unit else A -> unit)
   (e : A = B), f A true = f B true.
intros;  rewrite e; reflexivity.
Qed.

(* example that Congruence. can solve
(dependent function applied to the same argument)*)

Theorem dep3 :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x),
f = g -> forall x : A, f x = g x.  intros.
congruence.
Qed.

(* Examples with injection rule *)

Theorem inj1 :
forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d.
intros.
split;  congruence.
Qed.

Theorem inj2 :
forall (A : Set) (a c d : A) (f : A -> A * A),
f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
intros.
congruence.
Qed.

(* Examples with discrimination rule *)

Theorem discr1 : true = false -> False.
intros.
congruence.
Qed.

Theorem discr2 : Some true = Some false -> False.
intros.
congruence.
Qed.

(* example with implications *)

Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D  ->
(A -> C) = (B -> D).
congruence.
Qed.

Set Implicit Arguments.

Parameter elt: Set.
Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
Definition t (A: Set) := elt -> A.
Definition get (A: Set) (x: elt) (m: t A) := m x.
Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
    fun (y: elt) => if elt_eq y x then v else m y.
Lemma gsident:
  forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Proof.
  intros. unfold get, set. case (elt_eq j i); intro.
  congruence.
  auto.
Qed.

(* bug 2447 is now closed (PC, 2014) *)

Section bug_2447.

Variable T:Type.

Record R := mkR {x:T;y:T;z:T}.

Variables a a' b b' c c':T.

Lemma bug_2447: mkR a b c = mkR a' b c -> a = a'.
congruence.
Qed.

Lemma bug_2447_variant1: mkR a b c = mkR a b' c -> b = b'.
congruence.
Qed.

Lemma bug_2447_variant2: mkR a b c = mkR a b c' -> c = c'.
congruence.
Qed.

End bug_2447.

(* congruence was supposed to do discriminate but it was bugged for
   types with indices *)

Inductive I : nat -> Type := C : I 0 | D : I 0.
Goal ~C=D.
congruence.
Qed.

(* Example by Jonathan Leivant, congruence up to universes *)
Section JLeivant.
  Variables S1 S2 : Set.

  Definition T1 : Type := S1.
  Definition T2 : Type := S2.

  Goal T1 = T1.
    congruence.
    Undo.
    unfold T1.
    congruence.
  Qed.
End JLeivant.

(* An example with primitive projections *)

Module PrimitiveProjections.
Set Primitive Projections.
Record t (A:Type) := { f : A }.
Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
congruence.
Undo.
intros.
unfold f in H0. (* internally turn the projection to unfolded form *)
congruence.
Qed.
End PrimitiveProjections.

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