I want to create a function(fixpoint
to be specific) in Coq that takes two types as input and tells whether they are same or not. The signature of this function can be given as
Fixpoint areSame (X1 X2 : Type) : bool
Please let me know if it even possible or not.
I create a custom datatype as following
Inductive State : Type :=
| state : forall X:Type, X -> State.
Now i want to compare any two given strings. Lets say i want to compare two states formed as following,
state bool true , state bool false
In order to do so, i must first confirm both states are defined with type bool
, and then compare values with equivalence defined on bool
.
All help is highly appreciated.
It is not possible to do so in the term language (Gallina), because the term Type
is open, and so for instance you cannot pattern match on its elements.
I believe a solution to your problem is to define an inductive datatype of descriptions of types of states, along with their interpretation in terms of Type
:
Inductive StateType : Type :=
| Bool
.
Definition typeOfStateType (t : StateType) : Type :=
match t with
| Bool -> bool
end.
Inductive State : Type :=
| state : forall (st : StateType), typeOfStateType st -> State
.