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?

Also tried by delaying `rf`

binding but I guess that's not of much help since `τ`

has to be bound at the very beginning.

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'.
```

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?

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

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

(Note that the magic is now happening in how Coq compiles `head`

and `tail`

)

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

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

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.

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.

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

@Julin Shaji

Welcome in the *wonderfull world of dependent pattern matching* !!

I would advise to:

- write proof scripts first (cf @Quentin VERMANDE )
- then
`Print`

the term and study its structure - 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.
```

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?

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`

.

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

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

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