Stream: Coq users

Topic: Type deduction for Prop


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Julio Di Egidio (Nov 24 2023 at 20:16):

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

view this post on Zulip Julio Di Egidio (Nov 24 2023 at 20:29):

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

view this post on Zulip 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