Hi, I am trying to define proof for the base intuitionistic lemmas using Definitions; however, I receive errors that I cannot understand root causes.

```
From mathcomp Require Import ssreflect seq.
Section Intuitionistic_Propositional_Logic.
Definition A_impl_A (A : Prop) : A -> A := fun proof_A => proof_A.
Definition A_impl_B_impl_A (A B : Prop) : A -> (B -> A) := fun proof_A => fun proof_B => proof_A.
Inductive and (A B : Prop) : Prop :=
| conj of A & B.
Definition andC (A B : Prop) : and A B -> and B A :=
fun '(conj proof_A proof_B) => conj proof_B proof_A.
Definition andA (A B C : Prop) : and C (and A B) -> and A (and B C) :=
fun '(conj proof_C (conj proof_A proof_B)) => conj proof_A (conj proof_B proof_C).
Definition iff (A B : Prop) : Prop := and (A -> B) (B -> A).
End Intuitionistic_Propositional_Logic.
```

For `andC`

and `andA`

it says:

```
In environment
A : Prop
B : Prop
pat : and A B
proof_A : A
proof_B : B
The term "proof_B" has type "B" while it is expected to have type "Prop".
```

Please help me understand the reason and how to fix it.

The type arguments of `conj`

are not set to implicit, so this at least compiles, though I am not sure it actually works as you intended:

```
Definition andC (A B : Prop) : and A B -> and B A :=
fun '(conj proof_A proof_B) => conj B A proof_B proof_A.
Definition andA (A B C : Prop) : and C (and A B) -> and A (and B C) :=
fun '(conj proof_C (conj proof_A proof_B)) =>
conj A (and B C) proof_A (conj B C proof_B proof_C).
```

https://coq.inria.fr/refman/language/extensions/implicit-arguments.html

[DELETED: I am just not sure what is going on with that code...]

Julio Di Egidio said:

The type arguments of

`conj`

are not set to implicit, so this at least compiles, though I am not sure it actually works as you intended:`Definition andC (A B : Prop) : and A B -> and B A := fun '(conj proof_A proof_B) => conj B A proof_B proof_A. Definition andA (A B C : Prop) : and C (and A B) -> and A (and B C) := fun '(conj proof_C (conj proof_A proof_B)) => conj A (and B C) proof_A (conj B C proof_B proof_C).`

@Julio Di Egidio It works, thank you very much!

Last updated: Jun 23 2024 at 05:02 UTC