The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,

Just for fun :
Using Coq 8.6, if ty is an inductive defined as Inductive ty := TBool : ty | 
TNat : ty | TList : ty -> ty.
--8<----
Definition map_fusion t G (e : exp G t) :=
match e in exp _ t return exp G t with
 | emap _ t2 t1 g em => match em in exp _ (TList t2') 
                      return exp (t2'::G) t1 -> exp G (TList t1) with
                      | emap _ t3 t2'' f eb => fun g' => emap _ _ _ (compose 
_ _ _ _ g' f) eb
                      | em => fun _ => emap _ _ _ g em
                      end g
 |  e => e
end.
--8<----
works sadly only at 95% : Coq says : Error: Cannot infer an internal 
placeholder of type "Type". Too bad because it could take whatever it wants !
Therefore you have to either do
--8<----
Definition map_fusion t G (e : exp G t) : exp G t.
Proof.
refine
 (match e in exp _ t return exp G t with
 | emap _ t2 t1 g em => match em in exp _ (TList t2') 
                      return exp (t2'::G) t1 -> exp G (TList t1) with
                      | emap _ t3 t2'' f eb => fun g' => emap _ _ _ (compose 
_ _ _ _ g' f) eb
                      | em => fun _ => emap _ _ _ g em
                      end g
 |  e => e
end).
exact hilbert_paradox.
exact fermat_last_thoerem.
Defined.
--8<-----
or
--8<-----
Definition map_fusion t G (e : exp G t) : exp G t :=
match e in exp _ t return exp G t with
 | emap _ t2 t1 g em => match em in exp _ foo 
                      return match foo with
                                 | TList t2' => exp (t2'::G) t1 -> exp G 
(TList t1)
                                 | _ => True end with
                      | emap _ t3 t2'' f eb => fun g' => emap _ _ _ (compose 
_ _ _ _ g' f) eb
                      | (enil _ _ | econs _ _ _ _ | efilter _ _ _ _) as em => 
fun _ => emap _ _ _ g em
                      | _ => I
                      end g
 |  e => e
end.
--8<-----

Pierre B.
> Le 2 mai 2017 à 08:45, Christian Kjær Larsen 
> <christianden AT gmail.com>
>  a écrit :
> 
> 
> Hi,
> 
> I'm currently writing my bachelors thesis, and I'm hitting some problems 
> with pattern matching on dependent
> types, and I was wondering if you guys could help. It seems a bit difficult 
> to work with in Coq.
> 
> I'm trying to formalise a small array language using intrinsically typed
> syntax, de bruijn indices for binders and Adam Chlipalas heterogeneous list 
> implementation from his book.
> 
> The idea is that I want to implement some fusion rules (like 
> https://wiki.haskell.org/Fusion
> ), and prove them correct using a semantics encoded in Coq.
> 
> The syntax is like this
> 
> Inductive exp G : ty -> Type :=
> | evar : forall t, member t G -> exp G t
> | etrue : exp G TBool
> | efalse : exp G TBool
> | econst : nat -> exp G TNat
> | esucc : exp G TNat -> exp G TNat
> | enil : forall t, exp G (TList t)
> | econs : forall t, exp G t -> exp G (TList t) -> exp G (TList t)
> | emap : forall t1 t2, exp (t1 :: G) t2 -> exp G (TList t1) -> exp G (TList 
> t2)
> | efilter : forall t1, exp (t1 :: G) TBool -> exp G (TList t1) -> exp G 
> (TList t1).
> 
> And I have tried to define a fusion rule for (map f (map g) == map (f o g)) 
> like this
> 
> Definition map_fusion t G (e : exp G t) :=
>   match e in exp _ t return exp G t with
>   | emap t2 t1 g em => match em in exp _ (TList t3) return exp G t with
>                        | emap t3 t2 f eb => emap (compose f g) eb
>                        | _ => e
>                        end
>   |  _ => e
> end.
> 
> This does not work, because Coq does not know that the t2's are the
> same. Do you have any tips for doing this style of dependent pattern
> matching in Coq. I have tried to use the Program tactic, but I hit some
> kind of bug. (
> https://coq.inria.fr/bugs/show_bug.cgi?id=5473
> ).
> 
> I hope that my question makes sense, and that some of you will have the 
> time to answer.
> 
> Cheers,
> 
> Christian Kjær Larsen
> Student at the University of Copenhagen, Denmark.
> 
> 
>