✔ Error using theorem application as a Goal · Coq users

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.

Goal member 1 [1;2;3;4] = true -> member 1 (set_union [3;5;6] [1;2;3;4]) = true.
Proof.
  simpl. reflexivity. Qed.

Gaëtan Gilbert (Jun 25 2022 at 06:34):

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.

Pierre Castéran (Jun 25 2022 at 07:00):

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.

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

Extract Constant QuickChick.Test.defNumTests => "1000000".

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

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.

Jiahong Lee (Jun 26 2022 at 05:51):

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.

Jiahong Lee (Jun 26 2022 at 06:02):

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.

Jiahong Lee (Jun 26 2022 at 06:14):

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.

Goal prop_of(<theorem instance>).
Proof.
  unfold prop_of.
  <tactics>.

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

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.

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.

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

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

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.

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?

Jiahong Lee (Jun 27 2022 at 01:47):

Sorry, I don't understand what you meant by "types inhabited by their proofs" and "member_union_intro_r produces a proof" :sweat_smile:

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.

Jiahong Lee (Jun 27 2022 at 06:40):

Notification Bot (Jun 27 2022 at 06:40):

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.

Stream: Coq users

Topic: ✔ Error using theorem application as a Goal

Jiahong Lee (Jun 25 2022 at 02:35):