CODEWITHSUNDEEP
coq
Matias Haeussler
Matias Haeussler

Reputation: 1131

Interpret term as type in Coq

I am building Integers from Naturals bottom-up and trying to apply a morphism rewrite directly instead of adding it as a setoid morphism because in my case it is hard and unnatural to do it, but a test case is failing with the following error:

The term "x = x" has type "Prop" while it is expected to have type "x = x".

Which is also thrown by the following MRE:

Require Import Setoid.

(* Custom natural Set *)
Parameter CNat : Set.

(* Addition *) 
Parameter CAdd : CNat -> CNat -> CNat. 
Infix "±" := CAdd (at level 50, left associativity).

(* Addition Morphism *)
Axiom cnat_add_morphism : 
  forall (x x' : CNat), x = x' ->
  forall (y y' : CNat), y = y' -> 
    x ± y = x' ± y'.

(* Test Example *)
Example cnat_add_inc : 
  forall (x y c : CNat), x = y -> x±c = y±c.
Proof.
  intros x y c CH.
  rewrite (@cnat_add_morphism x x (x=x) c c (c=c)). (* #Error *)

Is it possible to tell cnat_add_morphism (which in my code is a theorem instead of an axiom) to interpret the terms x¦x and c¦c as a type to make the morphism work properly, or a different one to be able to apply a manual morphism rewrite instead of adding it as a setoid?

Upvotes: 0

Views: 183

Answers (2)

Kamyar Mirzavaziri
Kamyar Mirzavaziri

Reputation: 858

There are several problems here.

First of all, the error means you are trying to give cnat_add_morphism a proposition instead of a proof of that proposition. In Coq, proofs are objects of type of the proposition they are the proof of. for example, forall x : CNat, x¦x is a type and you have to build an object of that type to guarantee that the type is true. This is like you have a function f : nat -> nat and you write f nat, you get the following error:

The term "nat" has type "Set" while it is expected to have type "nat".

The error you are receiving is exactly the same. So you need to provide an object of type "x ¦ x" i.e., a proof that guarantees the proposition x ¦ x is true. So you can use the ceq_reflexivity axiom. The term (ceq_reflexivity x) has the type x¦x and you can use it instead of wrong usage of x¦x.

(cnat_add_morphism x x (ceq_reflexivity x))

Second, you need to apply the lemma not rewrite it and use the assumption instead of x¦x (use x and y not x only).

apply (cnat_add_morphism x y CH c c (ceq_reflexivity c)).

Upvotes: 1

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

The first problem you have is that the term you want to rewrite is not well-typed:

cnat_add_morphism x x (x¦x) c c (c¦c)

You have

cnat_add_morphism x x : x¦x -> forall y y', y¦y' -> x ± y ¦ x ± y'

so you need to provide a proof of x¦x but you're providing x¦x itself. You actually need to add proofs of reflexivity in your system. Something like

Parameter CRefl : forall (x : CNat), x¦x.

Then you can prove your lemma.

Example cnat_add_inc : 
  forall (x y c : CNat), 
    x¦y -> 
    x ± c ¦ y ± c.
Proof.
  intros x y c CH.
  apply cnat_add_morphism.
  - assumption.
  - apply CRefl.
Qed.

Upvotes: 1

Related Questions