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:

- Did I apply the theorem wrongly? Perhaps, syntax-wise?
- Is there a better way of substituting values (instantiating) a theorem to check whether its
`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).

- A computational proof (your proof with
`reflexivity`

) - As an application of your theorem:

```
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 like`apply (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:

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

@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 that`member_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