Tvals in my code is the total map, why coq insists it is not?

Using Coq
1

Hello, I am not able to make this code work.
I expect that tvals in formulaTrue inductive type is a total map. So I should be able to check in
TVar constructor if (tvals var) equals true or not. But Coq gives an error:

Error: Illegal application (Non-functional construction):
The expression “tvals” of type “Type” cannot be applied to the term
“var” : “?T”

Definition var := nat % type. 

Definition total_map (A : Type) := var -> A.

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

Definition t_update {A : Type} (m : total_map A)
                    (x : var) (v : A) :=
  fun x' => if PeanoNat.Nat.eqb x x' then v else m x'.

Definition tvals := total_map bool.

Inductive formula : Set :=
  | Var : var -> formula.

Inductive formulaTrue : tvals -> formula -> Prop :=
  | TVar : forall var, tvals var = true -> formulaTrue tvals (Var var).

Please advice, where is my mistake?

2

The identifier tvals in the definition of TVar should refer to an inhabitant of the type tvals that you define beforehand, so you should quantify over this identifier at the same time as var (and maybe rename it to tv to lessen the confusion):

Inductive formulaTrue : tvals -> formula -> Prop :=
  | TVar : forall tv var, tv var = true -> formulaTrue tv (Var var).
1 Like
3

Hello,

You have defined tvals as the type of functions from var to bool. You can therefore apply any element in this type to a variable, but not the type itself. Currently, it is as if you were trying to use var as a specific natural number.

You probably meant to write:

Inductive formulaTrue : tvals -> formula -> Prop :=
  | TVar : forall map var, map var = true -> formulaTrue map (Var var).

EDIT: Woops, too slow :slight_smile:

1 Like
4

Thank you, I got it.

1 Like