Stream: Coq users

Topic: Predicates


view this post on Zulip Felipe Lisboa (Aug 23 2023 at 07:59):

I have the following problem:

Variable A B : Type.
Program Definition some_predicate (a : A) : Prop.
Admitted.

Program Definition  some_function (a : A) (H : some_predicate a) : B.
Admitted.

Fail Definition foo (a: option A) (b: B) : Prop -> B :=
match a with
| None => fun _ => b
| Some a' => fun H => foo a' H
end

I'm met with the error: "The term "H" has type "Prop" while it is expected to have type "some_predicate a'".

some_function is a total function over type A and takes a predicate (H: some_predicate a). So, my question is, how can I introduce the predicate some_predicate a in the Some a branch of the match ?

Thanks!

view this post on Zulip Pierre Rousselin (Aug 23 2023 at 08:15):

Do you mean some function instead of foo in the body of the Fail Definition ?

view this post on Zulip Felipe Lisboa (Aug 23 2023 at 08:20):

Yes, exactly. My bad.

I already found the solution, however. some_function needs to be of type bool (which makes sense because it is a function), which allows me to pattern match on it.

Variable A B : Type.
Program Definition some_predicate (a : A) : bool.
Admitted.

Program Definition  some_function (a : A) (H : some_predicate a) : B.
Admitted.

Program Definition foo (a: option A) (b: B) : B :=
match a with
| None =>  b
| Some a' => match (some_predicate a') with
                          | false => b
                          | true => some_function a' _
                          end
end

view this post on Zulip Pierre Castéran (Aug 23 2023 at 08:41):

(deleted)


Last updated: Jun 13 2024 at 19:02 UTC