I sometimes have functions which return a type which is not convertible to the type I want. I then use an equality proof in a match construct like:

```
Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Definition proj_reptype_nested {cs : compspecs} (t : type) (gfs1 gfs2 : list gfield) (v : @reptype cs (nested_field_type t gfs1)) : @reptype cs (nested_field_type t (gfs2 ++ gfs1)) :=
match (nested_field_type_nested_field_type t gfs1 gfs2) in (_ = t2) return reptype t2 with
| eq_refl => (proj_reptype (nested_field_type t gfs1) gfs2 v)
end.
```

with

```
proj_reptype : forall (t : type) (gfs : list gfield), reptype t -> reptype (nested_field_type t gfs)
reptype : type -> Type
nested_field_type : type -> list gfield -> type
nested_field_type_nested_field_type : forall (t : type) (gfs0 gfs1 : list gfield),
nested_field_type (nested_field_type t gfs0) gfs1 = nested_field_type t (gfs1 ++ gfs0)
(a transparent lemma)
```

Now this works, and is not that inefficient, `nested_field_type_nested_field_type`

is a defined lemma and Ok to compute. Still the value of the computation is not used - there is only one possible constructor `eq_refl`

and its argument are not used. I wonder if there is some better trick to write functions with an equated return type, so that the equality proof is not in the computational path.

when the equality is decidable you can replace it with the decision, ie instead of `p : P`

you have `match decide P with yes p' => p' | no f => p (* or match f p with end *) end`

however whether that is more efficient is questionable

@Gaëtan Gilbert : so you propose to not keep the equality proof out of the computation chain, but make it faster by replacing it with a boolean decision procedure? This might give some advantage, but I am still looking for ways to keep the quality proof entirely out of the computation.

I experimented a bit with dependent records so that the type equality is "hidden" in some record fields which are in the end not evaluated when using lazy and a projection for the computational result, but couldn't make it work. Is there some high level type theoretic argument why the equality proof must be evaluated?

Consider the following code. If you do not explicitly evaluate `H`

, then you segfault:

```
Definition f (n : nat) (H : bool = nat) : bool :=
match H in (_ = T) return (T -> bool) with
| eq_refl => fun m : bool => m
end n.
```

depending on the type you're casting you can write a custom cast which doesn't need to compute the proof of equality

eg

```
Require Vector.
Fixpoint vec_cast {A} n m (v:Vector.t A n) : n = m -> Vector.t A m.
Proof.
destruct v as [|x n tl], m as [|m];intros e.
- constructor.
- exfalso; apply (O_S _ e).
- exfalso; apply (O_S _ (eq_sym e)).
- constructor.
+ exact x.
+ exact (vec_cast A n m tl (eq_add_S _ _ e)).
Defined.
```

`e`

is used only in the absurd branches

this effectively means you rebuild your terms when casting, so eg casting a vector is O(length of the vector)

since length of the vector = n using decidability of equality on nat is in the same O() class but maybe nicer to the GC(?)

@Guillaume Melquiond I see your point. On the other hand Coq is in almost all cases happy to know that a proof exists without evaluating it. Is it so that in this case an axiom `bool = nat`

would lead to a segfault and actually evaluating the proof term is the only way to know if it is an axiom?

Yes, that is the idea. (To be more precise, it can also be the consequence of an axiom.) For example, you can rewrite the example with `H`

of type `(bool -> bool) = (bool * bool)`

, which is a consequence of the univalence axiom.

when using Definitional UIP it's also possible to normalize reflexive equality proofs to refl, eg

```
Local Set Definitional UIP.
Inductive nat_eq (n:nat) : nat -> SProp := nat_eq_refl : nat_eq n n.
Unset Definitional UIP.
Arguments nat_eq_refl {_}.
Definition nat_eq_eq n m (e:nat_eq n m) : n = m := match e with nat_eq_refl => eq_refl end.
Definition eq_nat_eq n m (e:n = m) : nat_eq n m := match e with eq_refl => nat_eq_refl end.
Definition nf_eq_nat {n m} e := nat_eq_eq n m (eq_nat_eq n m e).
Eval lazy in fun n (e:n=n) => nf_eq_nat e.
(* fun n _ => eq_refl *)
```

however this only works with lazy, and while `nat`

should be safe doing it at arbitrary types breaks termination of lazy (and typechecking)

A variant of Gaëtan's idea is that you can sometimes recreate the `eq_refl`

constructor on the fly, thus avoiding matching on the original proof. For example, that is what the `erase`

function in Flocq. It can be used to drop an opaque proof and replace it with a transparent one:

```
Definition erase (x : binary_float) : binary_float.
Proof.
destruct x as [s|s| |s m e H].
- exact (B754_zero s).
- exact (B754_infinity s).
- exact B754_nan.
- apply (B754_finite s m e).
destruct bounded.
apply eq_refl. (* !!! *)
exact H.
Defined.
Theorem erase_correct : forall x, erase x = x.
```

(And Gaëtan just wrote the variant himself: `nf_eq_nat`

plays the same role as `erase`

.)

@Gaëtan Gilbert : thanks - I need to think about it. I guess the question is if I can make it such that the effort is proportional to the length of the field lists (gfs) - these are short and proportional to the nesting depth of structures in the C code, which is usually no more than 5. The `reptype`

of a struct is proportional to the total number of fields in a nested struct, and this can be large. In the end I need to show the equality of `reptype`

.

In essence my function computes the value of a field of a field from the value of the outer field (a struct) and needs to show that the type of a field of a field is the same as the type of the two field paths connected applied to the outer struct.

@Gaëtan Gilbert @Guillaume Melquiond : thanks for all the hints and explanations. In the end it will be tricky. I have 3 levels of objects here: lists of nested sub fields in a C struct, the types of C structs and the types of values of C structs. The latter two can be largish, only the first not. The type equality is on on of the large objects, but I guess I can make it such that some equality in the sub field lists leads to a convertible equality in the other types. I might need some intermediate structure for this. Thinking ...

Touch Sungkawichai has marked this topic as resolved.

Touch Sungkawichai has marked this topic as unresolved.

Gaëtan Gilbert said:

depending on the type you're casting you can write a custom cast which doesn't need to compute the proof of equality

eg`Require Vector. Fixpoint vec_cast {A} n m (v:Vector.t A n) : n = m -> Vector.t A m. Proof. destruct v as [|x n tl], m as [|m];intros e. - constructor. - exfalso; apply (O_S _ e). - exfalso; apply (O_S _ (eq_sym e)). - constructor. + exact x. + exact (vec_cast A n m tl (eq_add_S _ _ e)). Defined.`

`e`

is used only in the absurd branchesthis effectively means you rebuild your terms when casting, so eg casting a vector is O(length of the vector)

since length of the vector = n using decidability of equality on nat is in the same O() class but maybe nicer to the GC(?)

Excuse me for beginner's questions but how to prove that the typecasting work. That is, how to prove lemmas like this:

```
Lemma vec_cast_how: forall {A} n (v: Vector.t A n),
vec_cast v (eq_refl) = v.
```

Also if instead I use the one the author use originally with `eq_rect`

, how do I proceed from here:

```
Definition vec_cast' {A n m} (v: Vector.t A n) (H: n = m): Vector.t A m.
Proof.
replace m with n by H.
exact v.
Defined.
Lemma vec_cast'_: forall {A} n (v: Vector.t A n),
vec_cast' v (eq_refl) = v.
Proof.
intros. unfold vec_cast'. simpl_eq. reflexivity.
Qed.
Lemma vec_cast'2_how: forall {A} n m (v: Vector.t A n) (H: m = n),
vec_cast' (vec_cast' v (eq_sym H)) H = v.
Proof.
intros.
(* How to proceed *)
Qed.
```

@Touch Sungkawichai : not sure I understand your first question on `vec_cast_how`

correctly. It is a simple inductive proofs - see below.

The second question is more tricky - I guess you ask about how to use transitivity of equality here. The problem is that the intermediate value has a different type, so you need to have a concept of equality of different types. A common formalisation of this is called JMeq (afaik named after the former British PM John Major because he used to "compare apples with pears"). See the following Coq code how you can use JMeq here:

```
Require Import Vector.
Require Import JMeq.
Fixpoint vec_cast {A} n m (v:Vector.t A n) : n = m -> Vector.t A m.
Proof.
destruct v as [|x n tl], m as [|m];intros e.
- constructor.
- exfalso; apply (O_S _ e).
- exfalso; apply (O_S _ (eq_sym e)).
- constructor.
+ exact x.
+ exact (vec_cast A n m tl (eq_add_S _ _ e)).
Defined.
Lemma vec_cast_how: forall {A} n (v: Vector.t A n),
vec_cast n n v (eq_refl) = v.
Proof.
intros.
induction v.
- reflexivity.
- cbn. rewrite IHv. reflexivity.
Qed.
Definition vec_cast' {A n m} (v: Vector.t A n) (H: n = m): Vector.t A m.
Proof.
replace m with n by H.
exact v.
Defined.
Lemma vec_cast'JMeq: forall {A} n m (v: Vector.t A n) (H : n=m),
JMeq (vec_cast' v H) v.
Proof.
intros A n m v H.
unfold vec_cast', eq_rect.
destruct H.
apply JMeq_refl.
Qed.
Lemma vec_cast'2_how: forall {A} n m (v: Vector.t A n) (H: m = n),
vec_cast' (vec_cast' v (eq_sym H)) H = v.
Proof.
intros.
apply JMeq_eq.
eapply JMeq_trans; apply vec_cast'JMeq.
Qed.
```

Note that you can go from JMeq to eq only if the two types are convertible (equality is not enough). But as you can see you can use JMeq in cases where the type of intermediate values in a transitive judgment is just provably equal (not convertible), but the first and last value have convertible type.

In general equality between objects of non convertible (just equal) type is messy - one best avoids this situation. This is the reason that vector (afaik) is not really recommended to be used.

don't use jmeq for this, you can just

```
Require Import Vector.
Definition vec_cast' {A n m} (v: Vector.t A n) (H: n = m): Vector.t A m.
Proof.
rewrite <-H.
exact v.
Defined.
Lemma vec_cast'2_how: forall {A} n m (v: Vector.t A n) (H: m = n),
vec_cast' (vec_cast' v (eq_sym H)) H = v.
intros. destruct H. reflexivity.
Qed.
```

and vec_cast' is defined using eq_rect so you can use lemmas about eq_rect like

```
Lemma vec_cast'_trans {A} n m k (v:Vector.t A n) (H:n = m) (H':m = k)
: vec_cast' (vec_cast' v H) H' = vec_cast' v (eq_trans H H').
apply rew_compose.
Qed.
```

@Gaëtan Gilbert : I am not sure if the question was how to prove this specific lemma most effectively or how to prove the second lemma from the first using transitivity, which looks natural here but doesn't work without JMeq.

Btw.: The JMeq method pulls in axiom "Eqdep.Eq_rect_eq.eq_rect_eq" which one might want to avoid. Still one needs to be able to compose proofs if things get more complicated - and JMeq can be useful in such situations.

Thank you both for your answer.

by *convertible types*, you refer to the casting by construction as done in the `Fixpoint vec_cast`

, right?

So if types are convertible, it is better to opt for *convertible casting*, isn't it?

Convertible means that you can convert one term to another using Coq's reduction rules. E.g. in nat `3+4`

is convertible with `2+5`

. But e.g. `a+b`

is provably equal to `b+a`

, but these two terms are not convertible. You cannot compute by applying reduction rules that `a+b=b+a`

, you need an inductive proof for this. If terms are convertible there is no need for casting functions or the like - you can use the Coq tactic `change`

to replace a term with a convertible term - without giving any reason.

Thanks

Last updated: Jun 13 2024 at 19:02 UTC