CODEWITHSUNDEEP
coq
Helen
Helen

Reputation: 77

Construct Sets in Coq

How to construct elements of the following set(assuming A : Set)?

A -> A + A

My answer is following:

Definition set : A -> A + A :=
fun a => match a with
         | inl l => a
         | inr r => a
         end.

And it returns:

Error: In environment
P, Q, R : Prop
A, B, C : Set
a : A
The term "a" has type "A" while it is expected to have type "?T + ?T0".

Upvotes: 0

Views: 268

Answers (1)

Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

I don't know if I understand your problem correctly, but here's a solution.

Definition mkset {A : Set}: A -> A + A.
  intro a.
  left.
  assumption.
Defined.

The idea is to use tactics to build a function of type A -> A + A. Tactic intro corresponds to abstraction of parameter a. Tactic left allows us to choose to prove just the left hand side of A + A. Finally, assumption search the hypothesis for a proposition that fits the current goal and finish it, if such hypothesis exists in context.

Upvotes: 1

Related Questions