Stream: Coq users

Topic: Lookup env with dependent types


view this post on Zulip Julin Shaji (Nov 27 2023 at 16:35):

I had been trying to do something like that's mentioned in this article.

Made some preliminaries like:

Inductive type: Type :=
| BVal: type
| NVal: type
| Arrow: type -> type -> type.

Fixpoint typeDe (t: type): Type :=
  match t with
  | BVal => bool
  | NVal => nat
  | Arrow t1 t2 => (typeDe t1) -> (typeDe t2)
  end.

Inductive ref {A: Type}: A -> list A -> Type :=
| Here: forall (a:A) (ls:list A),
    ref a (a::ls)
| Further: forall (a x: A) (ls: list A),
    ref a ls -> ref a (x::ls).

Inductive env: list type -> Type :=
| ENil: env []
| ECons: forall (τs: list type) (τ: type),
    typeDe τ -> env τs -> env (τ::τs).

Now a way to access elements from env is needed.

A function like:

(* This structure doesn't type check *)
Fixpoint lookupEnv {τ: type} {τs: list type}
 (en: env τs) (rf: ref τ τs): typeDe τ :=
  match en with
  | ENil => (* Impossible case ∵ ref value [rf] is present *)
  | ECons _ _ v en' =>
      match rf with
      | Here _ _ => v
      | Further _ _ _ rf' => lookup en' rf'
    end
  end.

But how can can this be achieved while having the advantage of dependent types?

view this post on Zulip Julin Shaji (Nov 27 2023 at 16:46):

Also tried by delaying rfbinding but I guess that's not of much help since τ has to be bound at the very beginning.

view this post on Zulip Meven Lennon-Bertrand (Nov 27 2023 at 16:48):

If you are fine with using it, Equations has been designed for this type of tasks:

From Equations Require Import Equations.

Equations lookupEnv {τ: type} {τs: list type}
 (en: env τs) (rf: ref τ τs): typeDe τ :=
  lookupEnv (ECons _ _ v _) (Here _ _) := v ;
  lookupEnv (ECons _ _ _ en') (Further _ _ _ rf') := lookupEnv en' rf'.

view this post on Zulip Julin Shaji (Nov 27 2023 at 16:56):

Haven't used equations much yet. But I guess it's about time I did.

Would defining this function in vanilla coq involve too much gymnastics?

view this post on Zulip Meven Lennon-Bertrand (Nov 27 2023 at 17:03):

It will definitely require some gymnastics. The difficulty is in getting Coq convinced that 1) the inaccessible branch is indeed inaccessible and 2) that the types of the terms for the recursive call match as they should (both the types of en' and rf', and that of the whole lookupEnv en' rf' with what the function expects). It is not unfeasible, but requires some craft, that Equations neatly automatises. (If you want to have an idea of what happens, you can Print lookupEnv; it's obviously less nice than a term written by hand, but it should give you an idea of the type of patterns you would have to do by hand.)

view this post on Zulip Meven Lennon-Bertrand (Nov 27 2023 at 17:14):

Ok in this particular case you can go around the difficulties by factoring them out in a way that is tractable for Coq:

Definition head {τ τs} (en : env (τ :: τs)): typeDe τ :=
  match en with
  | ECons _ _ t _ => t
  end.

Definition tail {τ τs} (en : env (τ :: τs)): env τs :=
  match en with
  | ECons _ _ _ en' => en'
  end.

Fixpoint lookupEnv {τ: type} {τs: list type}
 (rf: ref τ τs) : env τs -> typeDe τ :=
  match rf with
    | Here _ _ => head
    | Further _ _ _ rf' => fun en => lookupEnv rf' (tail en)
  end.

view this post on Zulip Meven Lennon-Bertrand (Nov 27 2023 at 17:15):

(Note that the magic is now happening in how Coq compiles head and tail)

view this post on Zulip Meven Lennon-Bertrand (Nov 27 2023 at 17:15):

(And that I have sneakily changed the structure on which the induction is performed)

view this post on Zulip Quentin VERMANDE (Nov 27 2023 at 19:44):

You can also do it directly by hand quite easily. Simply put a point after giving the return type to enter proof mode and construct your term as if you were doing a proof. You would obtain something like that:

Fixpoint lookupEnv {τ: type} {τs: list type}
 (en: env τs) (rf: ref τ τs): typeDe τ.
Proof.
revert rf; destruct en as [|t ts]; intro in_nil; inversion in_nil.
  exact t0.
exact (lookupEnv _ _ en H1).
Defined.

view this post on Zulip Paolo Giarrusso (Nov 27 2023 at 21:15):

The challenge now is that the output of inversion is part of lookupEnv's public interface, and it's easy to use even less predictable tactics.

view this post on Zulip Paolo Giarrusso (Nov 27 2023 at 21:17):

Using a manual definition avoids that. And using Equations avoid that in large part, by providing a higher-level interface, that just exposes the defining equations as propositional equalities, usable for a rewriting system.

view this post on Zulip Paolo Giarrusso (Nov 27 2023 at 21:22):

Much of https://github.com/HoTT/Coq-HoTT/blob/master/STYLE.md#17-transparency-and-opacity applies here, including the list of recommended tactics.

view this post on Zulip Dominique Larchey-Wendling (Nov 29 2023 at 16:17):

@Julin Shaji

Welcome in the wonderfull world of dependent pattern matching !!

I would advise to:

  1. write proof scripts first (cf @Quentin VERMANDE )
  2. then Print the term and study its structure
  3. then use refine to rebuild, step by step, a term like the one below, cleaning up the one generated by the proof script which is usually too convoluted.

Over the long run, you might enjoy it ;-)

Inductive ref_cons_shape {A a} : forall x ls, ref a (x::ls) -> Type :=
| ref_cons_shape0 ls : ref_cons_shape a ls (Here a ls)
| ref_cons_shape1 x ls rf : ref_cons_shape x ls (@Further A a x ls rf).

Definition ref_shape A (a : A) l : ref a l -> Type :=
  match l with
  | []    => fun rf => Empty_set
  | x::ls => ref_cons_shape x ls
  end.

Lemma ref_inv {A a l} rf : ref_shape A a l rf.
Proof. destruct rf; constructor. Qed.

Fixpoint lookupEnv {τ: type} {τs: list type} (en: env τs) : ref τ τs -> typeDe τ :=
  match en in env τs' return ref τ τs' -> typeDe τ with
  | ENil           => fun rf =>
    match ref_inv rf with end
  | ECons τs τ T E => fun rf =>
    match ref_inv rf in ref_cons_shape t ls _ return typeDe t -> env ls -> _ with
    | ref_cons_shape0 _      => fun T _ => T
    | ref_cons_shape1 _ _ rf => fun _ E => lookupEnv E rf
    end T E
  end.

view this post on Zulip Julin Shaji (Dec 06 2023 at 11:48):

Paolo Giarrusso said:

The challenge now is that the output of inversion is part of lookupEnv's public interface, and it's easy to use even less predictable tactics.

And I didn't even know there was such a problem. :woozy_face:
Why is the term introduced by inversion unpredictable?

view this post on Zulip Paolo Giarrusso (Dec 06 2023 at 16:30):

I'm not saying inversion uses a random number generator, but I am saying that if it did, and proofs about lookupEnv break, that's a problem in lookupEnv.

view this post on Zulip Paolo Giarrusso (Dec 06 2023 at 16:33):

However, as it happens, https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Lookup.20env.20with.20dependent.20types/near/404478566 uses generated names, so that _definition_ will break as soon as I add an unused section assumption around the definition — something as simple as Section foo. Context (H : 1 = 1). ... End foo.

view this post on Zulip Paolo Giarrusso (Dec 06 2023 at 16:34):

to notice such problematic code, you can use Set Mangle Names.

view this post on Zulip Paolo Giarrusso (Dec 06 2023 at 16:35):

if you fix the proof, say to exact (lookupEnv _ _ en H2)., it's already possible that client proofs break, since ltac scripts need not respect alpha renaming. (I don't have a concrete example, I could probably write a contrived one but not sure it'd be convincing).


Last updated: Jun 23 2024 at 05:02 UTC