Quelle simple_congruence.v Sprache: Coq

Axiom P : Prop.
Definition Q := True -> P.

(* bug 13778, 5394 *)
Goal Q -> Q.
Proof.
  intro.
  Fail congruence.
  simple congruence.
Qed.

Goal (not P) -> P -> False.
Proof. simple congruence. Qed.

Goal (P -> False) -> not P.
Proof.
  simple congruence.
Qed.

Fixpoint slow (n: nat): bool :=
  match n with
  | O => true
  | S m => andb (slow m) (slow (pred m))
  end.

Parameter f: nat -> nat.

Definition foo(n b: nat): Prop :=
  if slow n then (forall a, f a = f b) else True.

(* fail fast symbolically *)
(* bug 13189 *)
Goal forall a b, foo 27 b -> f a = f b.
Proof.
  Timeout 1 Fail Time simple congruence.
  (* Fail Timeout 1 Time congruence. *)
Admitted.

(* succeed fast symbolically *)
(* bug 13189 *)
Goal forall a b, foo 29 b -> f b = f a -> f a = f b.
Proof.
  (* Fail Timeout 1 Time congruence. *)
  Timeout 1 simple congruence.
Qed.

Goal True -> not True -> P.
Proof. simple congruence. Qed.

(* consider final not *)
Goal False -> not True.
Proof. simple congruence. Qed.

(* consider final not *)
Goal not (true = false).
Proof. simple congruence. Qed.

Fixpoint stupid (n : nat) : unit :=
match n with
| 0 => tt
| S n =>
  let () := stupid n in
  let () := stupid n in
  tt
end.

(* do not try to unify 23 with stupid 23 *)
Goal 23 = 23 -> stupid 23 = stupid 23.
Proof. Timeout 1 simple congruence. Qed.

Inductive Fin : nat -> Set :=
| F1 : forall n : nat, Fin (S n)
| FS : forall n : nat, Fin n -> Fin (S n).

(* indexed inductives *)
Goal forall n (f : Fin n), FS n f = F1 n -> False.
Proof. intros n f H. simple congruence. Qed.

Axiom R : Prop.
Axiom R' : Prop.

Goal (not P) -> not P.
Proof. simple congruence. Qed.

Goal (P -> False) -> P -> False.
Proof. simple congruence. Qed.

Goal (not (true = true)) -> P.
Proof. simple congruence. Qed.

Goal Q -> (Q = R) -> R.
Proof. simple congruence. Qed.

(* unfortunately, common usecase *)
Goal P -> Q.
Proof.
  Fail simple congruence.
  repeat intro. simple congruence.
Qed.

(* bug 13778 *)
Goal R -> (R = not P) -> not P.
Proof.
  Fail congruence.
  simple congruence.
Qed.

Definition per_unit := forall u, match u with tt => True end.

(* bug 5394 *)
Goal per_unit -> per_unit.
Proof. simple congruence. Qed.

quality99%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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.