Julin Shaji (Nov 27 2023 at 16:35): 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?
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.
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'.
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?
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.)
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.
(Note that the magic is now happening in how Coq compiles head and tail)
Meven Lennon-Bertrand (Nov 27 2023 at 17:15):(And that I have sneakily changed the structure on which the induction is performed)
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.
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.
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.
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.
Dominique Larchey-Wendling (Nov 29 2023 at 16:17):@Julin Shaji
Welcome in the wonderfull world of dependent pattern matching !!
I would advise to:
Print the term and study its structurerefine 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?
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.
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.
Paolo Giarrusso (Dec 06 2023 at 16:34):to notice such problematic code, you can use Set Mangle Names.
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: Oct 13 2024 at 01:02 UTC