Skip to content

Fix some missing and incorrect Proof commands #254

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SkySkimmer merged 1 commit into from
Apr 2, 2026
Merged

Fix some missing and incorrect Proof commands #254

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions doc/sphinx/language/coq-library.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,7 @@ tactics (see Chapters ring and micromega), there are also:
From Stdlib Require Import DiscrR.
Open Scope R_scope.
Goal 5 <> 0.
Proof.
discrR.

.. tacn:: split_Rabs
Expand All @@ -187,6 +188,7 @@ tactics (see Chapters ring and micromega), there are also:
From Stdlib Require Import Reals.
Open Scope R_scope.
Goal forall x:R, x <= Rabs x.
Proof.
intro; split_Rabs.

.. tacn:: split_Rmult
Expand All @@ -201,6 +203,7 @@ tactics (see Chapters ring and micromega), there are also:
From Stdlib Require Import Reals.
Open Scope R_scope.
Goal forall x y z:R, x * y * z <> 0.
Proof.
intros; split_Rmult.

List library
Expand Down
Binary file modified test-suite/output/BinaryPrintingNotations.v
View file
Open in desktop
Binary file not shown.
4 changes: 4 additions & 0 deletions test-suite/output/FunExt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ From Stdlib Require Import FunctionalExtensionality.

(* Basic example *)
Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z).
Proof.
intro H.
extensionality in H.
symmetry in H.
Expand All @@ -11,6 +12,7 @@ Qed.

(* Test rejection of non-equality *)
Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''.
Proof.
intros H H' H''.
Fail extensionality in H.
clear H'.
Expand All @@ -20,6 +22,7 @@ Abort.

(* Test success on dependent equality *)
Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1.
Proof.
intros p H.
extensionality in p.
assumption.
Expand All @@ -28,6 +31,7 @@ Qed.
(* Test dependent functional extensionality *)
Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b),
(forall x y, f x y = g x y) -> f = g.
Proof.
intros * H.
extensionality in H.
assumption.
Expand Down
1 change: 1 addition & 0 deletions test-suite/output/Intuition.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
From Stdlib Require Import BinInt.
Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z.
Proof.
intros; intuition.
Show.
Abort.
2 changes: 2 additions & 0 deletions test-suite/output/RealNumberSyntax.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,11 +54,13 @@ Close Scope hex_R_scope.
From Stdlib Require Import Reals.

Goal 254e3 = 2540 * 10 ^ 2.
Proof.
ring.
Qed.

From Stdlib Require Import Psatz.

Goal 254e3 = 2540 * 10 ^ 2.
Proof.
lra.
Qed.
1 change: 1 addition & 0 deletions test-suite/output/allBytes.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,5 +120,6 @@ Notation "'~'" := (Byte.x7e) (only printing, at level 0).
Set Printing Depth 100.

Goal False.
Proof.
let cc := eval cbv in allBytes in idtac cc.
Abort.
121 changes: 61 additions & 60 deletions test-suite/output/simpl.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
(* Simpl with patterns *)

Goal forall x, 0+x = 1+x.
Proof.
intro x.
simpl (_ + x).
Show.
Expand Down Expand Up @@ -182,32 +183,32 @@ Check "DirectTuple (PrimitiveProjectionUnfolded)".
Record T := {p:nat}.
Definition a := {|p:=0|}.
Axiom P : nat -> Prop.
Goal P a.(p). unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
Goal P a.(p). unfold p. cbv delta [a]. cbn. Show. Abort. (* -> 0 *)
Goal P a.(p). unfold p. cbv delta [a]. hnf. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. cbn. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. hnf. Show. Abort. (* -> 0 *)
Arguments p : simpl never.
Goal P a.(p). unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
Goal P a.(p). unfold p. cbv delta [a]. cbn. Show. Abort. (* -> {| p := 0 |}.(p) *)
Goal P a.(p). unfold p. cbv delta [a]. hnf. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. cbn. Show. Abort. (* -> {| p := 0 |}.(p) *)
Goal P a.(p). Proof. unfold p. cbv delta [a]. hnf. Show. Abort. (* -> 0 *)
End DirectTuple.

Module NamedTuple.
Check "NamedTuple (PrimitiveProjectionUnfolded)".
Record T := {p:nat}.
Definition a := {|p:=0|}.
Axiom P : nat -> Prop.
Goal P a.(p). unfold p. simpl. Show. Abort. (* -> 0 *)
Goal P a.(p). unfold p. cbn. Show. Abort. (* -> 0 *)
Goal P a.(p). unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Goal P a.(p). Proof. unfold p. simpl. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. cbn. Show. Abort. (* -> 0 *)
Goal P a.(p). Proof. unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Arguments p : simpl never.
Goal P a.(p). unfold p. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
Goal P a.(p). unfold p. cbn. Show. Abort. (* -> a.(p) *)
Goal P a.(p). unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Goal P a.(p). Proof. unfold p. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
Goal P a.(p). Proof. unfold p. cbn. Show. Abort. (* -> a.(p) *)
Goal P a.(p). Proof. unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Arguments p : simpl nomatch.
Arguments a : simpl never.
Goal P a.(p). unfold p. simpl. Show. Abort. (* -> 0 *) (* bug never 1 *)
Goal P a.(p). unfold p. cbn. Show. Abort. (* -> a.(p) *)
Goal P a.(p). unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Goal P a.(p). Proof. unfold p. simpl. Show. Abort. (* -> 0 *) (* bug never 1 *)
Goal P a.(p). Proof. unfold p. cbn. Show. Abort. (* -> a.(p) *)
Goal P a.(p). Proof. unfold p. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
End NamedTuple.

Module DirectCoFix.
Expand All @@ -216,13 +217,13 @@ CoInductive U := {q:U}.
CoFixpoint a := {|q:=a|}.
Abbreviation COFIX := (cofix a := {|q:=a|}).
Axiom P : U -> Prop.
Goal P a.(q). unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *)
Goal P a.(q). unfold q. cbv delta [a]. cbn. Show. Abort. (* -> COFIX *)
Goal P a.(q). unfold q. cbv delta [a]. hnf. Show. Abort. (* -> COFIX *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. cbn. Show. Abort. (* -> COFIX *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. hnf. Show. Abort. (* -> COFIX *)
Arguments q : simpl never.
Goal P a.(q). unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *) (* never not respected on purpose *)
Goal P a.(q). unfold q. cbv delta [a]. cbn. Show. Abort. (* -> COFIX.(q) *)
Goal P a.(q). unfold q. cbv delta [a]. hnf. Show. Abort. (* -> COFIX *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *) (* never not respected on purpose *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. cbn. Show. Abort. (* -> COFIX.(q) *)
Goal P a.(q). Proof. unfold q. cbv delta [a]. hnf. Show. Abort. (* -> COFIX *)
End DirectCoFix.

Module NamedCoFix.
Expand All @@ -231,18 +232,18 @@ CoInductive U := {q:U}.
CoFixpoint a := {|q:=a|}.
Abbreviation COFIX := (cofix a := {|q:=a|}).
Axiom P : U -> Prop.
Goal P a.(q). unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). unfold q. cbn. Show. Abort. (* -> a *)
Goal P a.(q). unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P a.(q). Proof. unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). Proof. unfold q. cbn. Show. Abort. (* -> a *)
Goal P a.(q). Proof. unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Arguments q : simpl never.
Goal P a.(q). unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). unfold q. cbn. Show. Abort. (* -> a.(q) *)
Goal P a.(q). unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P a.(q). Proof. unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). Proof. unfold q. cbn. Show. Abort. (* -> a.(q) *)
Goal P a.(q). Proof. unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Arguments q : simpl nomatch.
Arguments a : simpl never.
Goal P a.(q). unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). unfold q. cbn. Show. Abort. (* -> a.(q) *)
Goal P a.(q). unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P a.(q). Proof. unfold q. simpl. Show. Abort. (* -> a *)
Goal P a.(q). Proof. unfold q. cbn. Show. Abort. (* -> a.(q) *)
Goal P a.(q). Proof. unfold q. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
End NamedCoFix.
End PrimitiveProjectionUnfolded.

Expand All @@ -257,64 +258,64 @@ Record T := {p:nat}.
Abbreviation TUPLE := {|p:=0|}.
Definition a := {|p:=0|}.
Axiom P : nat -> Prop.
Goal P (id p a). unfold id. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
Goal P (id p a). unfold id. cbv delta [a]. cbn. Show. Abort. (* -> 0 *)
Goal P (id p a). unfold id. cbv delta [a]. hnf. Show. Abort. (* -> TUPLE.(p) *) (* bug primproj 1 *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. cbn. Show. Abort. (* -> 0 *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. hnf. Show. Abort. (* -> TUPLE.(p) *) (* bug primproj 1 *)
Arguments p : simpl never.
Goal P (id p a). unfold id. cbv delta [a]. simpl. Show. Abort. (* -> TUPLE.(p) *)
Goal P (id p a). unfold id. cbv delta [a]. cbn. Show. Abort. (* -> TUPLE.(p) *)
Goal P (id p a). unfold id. cbv delta [a]. hnf. Show. Abort. (* -> TUPLE.(p) *) (* bug primproj 1 *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. simpl. Show. Abort. (* -> TUPLE.(p) *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. cbn. Show. Abort. (* -> TUPLE.(p) *)
Goal P (id p a). Proof. unfold id. cbv delta [a]. hnf. Show. Abort. (* -> TUPLE.(p) *) (* bug primproj 1 *)
End DirectTuple.

Module NamedTuple.
Check "NamedTuple (PrimitiveProjectionConstant)".
Record T := {p:nat}.
Definition a := {|p:=0|}.
Axiom P : nat -> Prop.
Goal P (id p a). unfold id. simpl. Show. Abort. (* -> 0 *)
Goal P (id p a). unfold id. cbn. Show. Abort. (* -> 0 *)
Goal P (id p a). unfold id. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Goal P (id p a). Proof. unfold id. simpl. Show. Abort. (* -> 0 *)
Goal P (id p a). Proof. unfold id. cbn. Show. Abort. (* -> 0 *)
Goal P (id p a). Proof. unfold id. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Arguments p : simpl never.
Goal P (id p a). unfold id. simpl. Show. Abort. (* -> a.(p) *)
Goal P (id p a). unfold id. cbn. Show. Abort. (* -> a.(p) *)
Goal P (id p a). unfold id. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Goal P (id p a). Proof. unfold id. simpl. Show. Abort. (* -> a.(p) *)
Goal P (id p a). Proof. unfold id. cbn. Show. Abort. (* -> a.(p) *)
Goal P (id p a). Proof. unfold id. hnf. Show. Abort. (* -> a.(p) *) (* bug primproj 2 *)
Arguments p : simpl nomatch.
Arguments a : simpl never.
Goal P (id p a). unfold id. simpl. Show. Abort. (* -> 0 *) (* never not respected on purpose *)
Goal P (id p a). unfold id. cbn. Show. Abort. (* -> a.(p) *)
Goal P (id p a). unfold id. hnf. Show. Abort. (* -> a.(p) *)
Goal P (id p a). Proof. unfold id. simpl. Show. Abort. (* -> 0 *) (* never not respected on purpose *)
Goal P (id p a). Proof. unfold id. cbn. Show. Abort. (* -> a.(p) *)
Goal P (id p a). Proof. unfold id. hnf. Show. Abort. (* -> a.(p) *)
End NamedTuple.

Module DirectCoFix.
Check "DirectCoFix (PrimitiveProjectionConstant)".
CoInductive U := {q:U}.
Abbreviation COFIX := (cofix a := {|q:=a|}).
Axiom P : U -> Prop.
Goal P (id q COFIX). unfold id. simpl. Show. Abort. (* -> COFIX *)
Goal P (id q COFIX). unfold id. cbn. Show. Abort. (* -> COFIX *)
Goal P (id q COFIX). unfold id. hnf. Show. Abort. (* -> COFIX.(q) *) (* bug primproj 3 *)
Goal P (id q COFIX). Proof. unfold id. simpl. Show. Abort. (* -> COFIX *)
Goal P (id q COFIX). Proof. unfold id. cbn. Show. Abort. (* -> COFIX *)
Goal P (id q COFIX). Proof. unfold id. hnf. Show. Abort. (* -> COFIX.(q) *) (* bug primproj 3 *)
Arguments q : simpl never.
Goal P (id q COFIX). unfold id. simpl. Show. Abort. (* -> COFIX.(q) *)
Goal P (id q COFIX). unfold id. cbn. Show. Abort. (* -> COFIX.(q) *)
Goal P (id q COFIX). unfold id. hnf. Show. Abort. (* -> COFIX.(q) *) (* bug primproj 3 *)
Goal P (id q COFIX). Proof. unfold id. simpl. Show. Abort. (* -> COFIX.(q) *)
Goal P (id q COFIX). Proof. unfold id. cbn. Show. Abort. (* -> COFIX.(q) *)
Goal P (id q COFIX). Proof. unfold id. hnf. Show. Abort. (* -> COFIX.(q) *) (* bug primproj 3 *)
End DirectCoFix.

Module NamedCoFix.
Check "NamedCoFix (PrimitiveProjectionConstant)".
CoInductive U := {q:U}.
CoFixpoint a := {|q:=a|}.
Axiom P : U -> Prop.
Goal P (id q a). unfold id. simpl. Show. Abort. (* -> a *)
Goal P (id q a). unfold id. cbn. Show. Abort. (* -> a *)
Goal P (id q a). unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P (id q a). Proof. unfold id. simpl. Show. Abort. (* -> a *)
Goal P (id q a). Proof. unfold id. cbn. Show. Abort. (* -> a *)
Goal P (id q a). Proof. unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Arguments q : simpl never.
Goal P (id q a). unfold id. simpl. Show. Abort. (* -> a.(q) *)
Goal P (id q a). unfold id. cbn. Show. Abort. (* -> a.(q) *)
Goal P (id q a). unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P (id q a). Proof. unfold id. simpl. Show. Abort. (* -> a.(q) *)
Goal P (id q a). Proof. unfold id. cbn. Show. Abort. (* -> a.(q) *)
Goal P (id q a). Proof. unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Arguments q : simpl nomatch.
Arguments a : simpl never.
Goal P (id q a). unfold id. simpl. Show. Abort. (* -> a *) (* never not respected on purpose *)
Goal P (id q a). unfold id. cbn. Show. Abort. (* -> a.(q) *)
Goal P (id q a). unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
Goal P (id q a). Proof. unfold id. simpl. Show. Abort. (* -> a *) (* never not respected on purpose *)
Goal P (id q a). Proof. unfold id. cbn. Show. Abort. (* -> a.(q) *)
Goal P (id q a). Proof. unfold id. hnf. Show. Abort. (* -> a.(q) *) (* bug primproj 4 *)
End NamedCoFix.
End PrimitiveProjectionConstant.
3 changes: 0 additions & 3 deletions test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1934,14 +1934,12 @@ Qed.

Lemma Zsgn_19 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 < x + y)%Z.
Proof.
Proof.
intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
discriminate H || (constructor || apply Zsgn_12; assumption).
Qed.

Lemma Zsgn_20 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x + y < 0)%Z.
Proof.
Proof.
intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
discriminate H || (constructor || apply Zsgn_11; assumption).
Qed.
Expand All @@ -1955,7 +1953,6 @@ Qed.

Lemma Zsgn_22 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x <= 0)%Z.
Proof.
Proof.
intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
discriminate H || discriminate H0.
Qed.
Expand Down
3 changes: 1 addition & 2 deletions test-suite/success/Nsatz.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,8 +284,7 @@ Lemma Thales: forall O A B C D:point,
(distance2 O B * distance2 O C = distance2 O D * distance2 O A
/\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
\/ collinear O A B.
geo_begin.
Proof.
Proof. geo_begin.
idtac "Thales 2 goals".
Time nsatz.
Time nsatz.
Expand Down
Loading