## Stream: Coq users

### Topic: Type deduction for Prop

#### Georgii (Nov 24 2023 at 16:54):

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

#### Julio Di Egidio (Nov 24 2023 at 20:05):

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 (Nov 24 2023 at 20:16):

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

#### Julio Di Egidio (Nov 24 2023 at 20:29):

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

#### Georgii (Nov 25 2023 at 08:50):

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