The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello, 

When I am not clever enough to write a dependent matchp, I enter the
proof mode: tactics are actually pretty good at generating return
clauses. 
After the Defined, I ask for the proof term and then removes some
noise.

In the proof, when I intend to perform a case analysis, I am careful to
only do it on terms which type parameters are variables.
If not, I use the remember tactic to get an equality. 
(The equality is usually needed to rewrite inside types.)

This simple strategy is usually enough.

Best,

--
Frédéric



On Tue, 2017-05-02 at 14:45 +0200, Christian Kjær Larsen wrote:
> 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.
> 
>