Stream: Coq users

Topic: ✔ Error using theorem application as a Goal


view this post on Zulip Jiahong Lee (Jun 25 2022 at 02:35):

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:

  1. Did I apply the theorem wrongly? Perhaps, syntax-wise?
  2. Is there a better way of substituting values (instantiating) a theorem to check whether its True? (My main goal)

Thanks!

view this post on Zulip Gaëtan Gilbert (Jun 25 2022 at 06:34):

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

view this post on Zulip Michael Soegtrop (Jun 25 2022 at 06:59):

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.

view this post on Zulip Pierre Castéran (Jun 25 2022 at 07:00):

That's not weird. You have two ways of proving your goal (two proofs).

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.

view this post on Zulip Michael Soegtrop (Jun 25 2022 at 07:06):

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.

view this post on Zulip Michael Soegtrop (Jun 25 2022 at 07:09):

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 ...

view this post on Zulip Jiahong Lee (Jun 26 2022 at 05:38):

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...

view this post on Zulip Jiahong Lee (Jun 26 2022 at 05:51):


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.

view this post on Zulip Jiahong Lee (Jun 26 2022 at 06:02):

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.

view this post on Zulip Jiahong Lee (Jun 26 2022 at 06:14):


@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:

  1. Can I abstract this pattern into a custom Command or a Definition? Perhaps a user-defined macro?
    That's, this:
Goal prop_of(<theorem instance>).
Proof.
  unfold prop_of.
  <tactics>.

into

Instance_goal <theorem instance>.
Proof.
  <tactics>.

view this post on Zulip Jiahong Lee (Jun 26 2022 at 06:30):


@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.

view this post on Zulip Jiahong Lee (Jun 26 2022 at 06:34):

Ah, my apology. To use the correct terminology, so member_union_intro_r is a Conjecture that I want to prove to be true.

view this post on Zulip Jiahong Lee (Jun 26 2022 at 06:38):


@Michael Soegtrop Thanks! Didn't know that QuickChick can do this. I'll stick to manual checking for now while learning how QuickChick works

view this post on Zulip Paolo Giarrusso (Jun 26 2022 at 13:13):

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

view this post on Zulip Jiahong Lee (Jun 27 2022 at 01:20):

@Paolo Giarrusso Thanks, member_union_intro_r x l1 l2 : member_union_intro_r_fun x l1 l2 : Propis 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.

view this post on Zulip Jiahong Lee (Jun 27 2022 at 01:41):


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?

view this post on Zulip Jiahong Lee (Jun 27 2022 at 01:47):

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:

view this post on Zulip Pierre Castéran (Jun 27 2022 at 05:37):

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

view this post on Zulip Jiahong Lee (Jun 27 2022 at 06:40):

Thanks! I'll reach there soon. Currently at last chapter of SF volume 0.

I'll consider my original question as solved.

view this post on Zulip Notification Bot (Jun 27 2022 at 06:40):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip Pierre Courtieu (Jun 27 2022 at 07:36):

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: Mar 28 2024 at 11:01 UTC