Stream: Coq users

Topic: How to keep equality proofs out of the computational path


view this post on Zulip Michael Soegtrop (Feb 08 2024 at 19:34):

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.

view this post on Zulip Gaëtan Gilbert (Feb 08 2024 at 20:04):

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

view this post on Zulip Michael Soegtrop (Feb 09 2024 at 09:32):

@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.

view this post on Zulip Michael Soegtrop (Feb 09 2024 at 09:35):

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?

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 09:40):

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.

view this post on Zulip Gaëtan Gilbert (Feb 09 2024 at 09:46):

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(?)

view this post on Zulip Michael Soegtrop (Feb 09 2024 at 09:47):

@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?

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 09:50):

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.

view this post on Zulip Gaëtan Gilbert (Feb 09 2024 at 09:57):

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)

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 09:58):

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.

view this post on Zulip Guillaume Melquiond (Feb 09 2024 at 10:01):

(And Gaëtan just wrote the variant himself: nf_eq_nat plays the same role as erase.)

view this post on Zulip Michael Soegtrop (Feb 09 2024 at 10:01):

@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.

view this post on Zulip Michael Soegtrop (Feb 09 2024 at 10:47):

@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 ...

view this post on Zulip Notification Bot (Feb 10 2024 at 03:24):

Touch Sungkawichai has marked this topic as resolved.

view this post on Zulip Notification Bot (Feb 10 2024 at 03:24):

Touch Sungkawichai has marked this topic as unresolved.

view this post on Zulip Touch Sungkawichai (Feb 10 2024 at 04:07):

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 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(?)

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.

view this post on Zulip Michael Soegtrop (Feb 10 2024 at 11:22):

@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.

view this post on Zulip Michael Soegtrop (Feb 10 2024 at 11:27):

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.

view this post on Zulip Michael Soegtrop (Feb 10 2024 at 11:28):

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.

view this post on Zulip Gaëtan Gilbert (Feb 10 2024 at 12:25):

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.

view this post on Zulip Gaëtan Gilbert (Feb 10 2024 at 12:30):

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.

view this post on Zulip Michael Soegtrop (Feb 10 2024 at 14:05):

@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.

view this post on Zulip Michael Soegtrop (Feb 10 2024 at 14:11):

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.

view this post on Zulip Touch Sungkawichai (Feb 10 2024 at 16:14):

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?

view this post on Zulip Michael Soegtrop (Feb 11 2024 at 09:16):

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.

view this post on Zulip Touch Sungkawichai (Feb 13 2024 at 03:52):

Thanks


Last updated: Jun 13 2024 at 19:02 UTC