Type deduction for Prop · Coq users

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

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

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: Oct 13 2024 at 01:02 UTC