Hi, given a theorem:
Theorem member_union_intro_r : forall (x : nat) (l1 l2 : list nat),
member x l1 = true -> member x (set_union l2 l1) = true.
I want to substitute values into a theorem to check whether it's True
. Intuitively, I thought I can apply theorem like a function. But I got an error doing this:
Goal member_union_intro_r 1 [1;2;3;4] [3;5;6].
Error: The term "member_union_intro_r 1 [1; 2; 3; 4] [3; 5; 6]" has type
"member 1 [1; 2; 3; 4] = true -> member 1 (set_union [3; 5; 6] [1; 2; 3; 4]) = true" which should be Set, Prop or Type.
That's weird because I have no problem doing this:
Goal member 1 [1;2;3;4] = true -> member 1 (set_union [3;5;6] [1;2;3;4]) = true.
Proof.
simpl. reflexivity. Qed.
Questions:
True
? (My main goal)Thanks!
You're confusing term and type
But I got an error doing this:
That's like doing Goal 0.
That's weird because I have no problem doing this:
and this is like doing Goal nat.
Is there a better way of substituting values (instantiating) a theorem to check whether its
True
? (My main goal)
I don't understand what you mean, if you have a proof then it is true
Let me elaborate a bit on @Gaëtan Gilbert 's answer since at the beginning this is hard to understand.
Please have a look at the following lines:
Require Import List.
Import ListNotations.
Axiom member : nat -> list nat -> bool.
Axiom set_union : list nat -> list nat -> list nat.
Theorem member_union_intro_r : forall (x : nat) (l1 l2 : list nat),
member x l1 = true -> member x (set_union l2 l1) = true.
Admitted.
Check member_union_intro_r 1 [1;2;3;4] [3;5;6].
(* Has type ": member 1 [1; 2; 3; 4] = true -> member 1 (set_union [3; 5; 6] [1; 2; 3; 4]) = true" *)
Check member 1 [1; 2; 3; 4] = true -> member 1 (set_union [3; 5; 6] [1; 2; 3; 4]) = true.
(* Has type Prop *)
Definition prop_of {P : Prop} (p : P) := P.
Check prop_of(member_union_intro_r 1 [1;2;3;4] [3;5;6]).
(* Has type Prop *)
Goal prop_of(member_union_intro_r 1 [1;2;3;4] [3;5;6]).
cbv.
That's not weird. You have two ways of proving your goal (two proofs).
reflexivity
)Example Ex1: member 1 [1;2;3;4] = true ->
member 1 (set_union [3;5;6] [1;2;3;4]) = true.
Proof. apply member_union_intro_r. Qed.
You can look at the associated proof terms with Print Ex1
for instance.
One more note: the easiest way to check if your lemma is likely true is QuickChick. If you use only well known data structures like nat and list, it should work out of the box. If you have your own data structures, you need to define a few things to make it work, but your case should be fine.
This should work (I can't check because I lack the definitions for your functions):
From QuickChick Require Import QuickChick.
Conjecture member_union_intro_r' : forall (x : nat) (l1 l2 : list nat),
member x l1 = true -> member x (set_union l2 l1) = true.
QuickChick member_union_intro_r'.
If you want to be more confident, you can do
Extract Constant QuickChick.Test.defNumTests => "1000000".
before you call QuickChick.
In my experience it is worthwhile to setup QuickChick for your own data structures - at least initially it takes a bit of time, but overall it is a great time saver. One can really spend a lot of time trying to prove something which is wrong ...
Ah, I'm surprised to find out that member_union_intro_r 1 [1;2;3;4] [3;5;6]
doesn't have type Prop
.
Since I can do something likeapply (member_union_intro_r x' l1' l2' H')
, I thought "theorem application" works like a function application, such that member_union_intro_r 1 [1;2;3;4] [3;5;6]
will be "evaluated" as member 1 [1;2;3;4] = true -> member 1 (set_union [3;5;6] [1;2;3;4]) = true
and thus has type Prop
.
Ok, I was wrong...
I don't understand what you mean, if you have a proof then it is true
Ya, iff I'm sure that the theorem is true. As a Coq beginner, if I couldn't prove my own theorems to be true, I can't be sure whether it's my theorems or my proofs (or both!) being wrong.
To handle that, I come up with an idea to "unit test" my theorem---simply substituting a few concrete values into my theorems to see how it works. Hence, my question (2) above.
Oh, on a second thought, I could indeed define a function for my purpose:
Definition member_union_intro_r_fun x l1 l2 :=
member x l1 = true -> member x (set_union l2 l1) = true.
Goal member_union_intro_r_fun 1 [1;2;3;4] [3;5;6].
Proof.
unfold member_union_intro_r_fun.
simpl. reflexivity. Qed.
Goal member_union_intro_r_fun 3 [1;2;3;4] [3;5;6].
Proof.
unfold member_union_intro_r_fun.
simpl. reflexivity. Qed.
This is what I'm looking for after all. I naively thought that Goal member_union_intro_r 1 [1;2;3;4] [3;5;6].
works the same.
@Michael Soegtrop :
Definition prop_of {P : Prop} (p : P) := P.
Wow, this is mind-blowing! Didn't know that I can return the inferred type! Not familiar with the cbv
tactic, but I'd do something like this:
Goal prop_of(member_union_intro_r 1 [1;2;3;4] [3;5;6]).
Proof.
unfold prop_of.
simpl. reflexivity. Qed.
Related question:
Command
or a Definition
? Perhaps a user-defined macro?Goal prop_of(<theorem instance>).
Proof.
unfold prop_of.
<tactics>.
into
Instance_goal <theorem instance>.
Proof.
<tactics>.
@Pierre Castéran Thanks, I appreciate it. But it's orthogonal to my question. My problem is that I'm not sure whether member_union_intro_r
is indeed True
, so I want to check it for a few instances.
Ah, my apology. To use the correct terminology, so member_union_intro_r
is a Conjecture
that I want to prove to be true.
@Michael Soegtrop Thanks! Didn't know that QuickChick can do this. I'll stick to manual checking for now while learning how QuickChick works
once you have defined member_union_intro_r_fun x l1 l2 : Prop
, then you have that member_union_intro_r x l1 l2 : member_union_intro_r_fun x l1 l2 : Prop
(where a : b : c
is an informal shortcut for a : b
and b : c
; Coq does not accept this shortcut). That is, your member_union_intro_r_fun x l1 l2
produces a Prop
that is your theorem statement; and in Coq, statements are types that are inhabited by their proofs, so your member_union_intro_r
produces a proof
@Paolo Giarrusso Thanks, member_union_intro_r x l1 l2 : member_union_intro_r_fun x l1 l2 : Prop
is a nice way seeing it. So I can read it as: member_union_intro_r x l1 l2
is a theorem with the statement member_union_intro_r_fun x l1 l2
of type Prop
.
Now that I know member_union_intro_r x l1 l2
has type member_union_intro_r_fun x l1 l2
. I still don't get why there is need for a type indirection:
Why can't Coq make it such thatmember_union_intro_r
has type Prop
right away? In other words, why member_union_intro_r x l1 l2 : member_union_intro_r_fun x l1 l2 : Prop
instead of member_union_intro_r x l1 l2 : Prop
where member_union_intro_r x l1 l2 = member_union_intro_r_fun x l1 l2
?
My explanation is that a proposition such as member_union_intro_r_fun
might be True
or False
depending on the values of the variables. But a theorem, by definition, is a True
statement. So a theorem can only be a subtype of proposition. Hence member_union_intro_r x l1 l2 : member_union_intro_r_fun x l1 l2 : Prop
. Is this correct?
in Coq, statements are types that are inhabited by their proofs, so your
member_union_intro_r
produces a proof
Sorry, I don't understand what you meant by "types inhabited by their proofs" and "member_union_intro_r
produces a proof" :sweat_smile:
I would not say "a theorem is by definition a true statement" but "a theorem is a statement which has some proof". Such a proof is a term whose type is the theorem's statement.
A clear explanation of the relation between the notions of theorems/proofs, and Coq's type system can be found for instance in https://softwarefoundations.cis.upenn.edu/current/lf-current/Logic.html
Thanks! I'll reach there soon. Currently at last chapter of SF volume 0.
I'll consider my original question as solved.
Jiahong Lee has marked this topic as resolved.
I think it is worth saying that « being true » or « being True » is very misleading here. Proving a theorem does not mean it is (equal to) True
or true
. Like not at all.
Last updated: Oct 01 2023 at 18:01 UTC