The Coq mailing list

[t x <txrev319 AT gmail.com>]

I've written the following example. Assertion 4 seems to imply that the type of E need not be fixed.

Can someone verify that the assertions / reasoning are correct? (All I know is that Coq accepts the definition, not whether Coq accepts the definition for the reason I think it accepts it).

Inductive Cat : Type := cat.
Inductive Dog : Type := dog.



(* Assertion 1: This fails because Coq can't infer this. *)
(*
Definition weird (b: bool) :=
  match b
    | true => cat
    | false => dog
  end.
*)



(* Assertion 2: this works because if we provide the type, it's a valid type *)
Definition weird (b: bool) :=
  match b as y in bool return (if y then Cat else Dog) with
    | true => cat
    | false => dog
  end.


(* Assertion 3: this can not work since
      (weird b) has type (if b then Cat else Dog), which
      does not fall into (T x1 x2 ... xn) *)
(*
Definition can_not_work (b: bool) :=
  match (weird b) as ... in ... return ... with
      ...
      end.

This can not possibly work since (weird b) has type
  (if b then Cat else Dog), which doesn't fall into
  T x1 x2 ... xn

 *)


Inductive iList : nat -> Set :=
| INil : iList O
| ICons : forall n, nat -> iList n -> iList (S n).

Fixpoint sum {n: nat} (lst: iList n) :=
  match lst with
    | INil => 0
    | ICons n x xs => x + (sum xs)
  end.


Require Import ZArith.

(* Assertion 4: the type of lst doesn't have to be fixed
   Our return type can be function of both the
     _value_ AND _type_ of the discremee *)
Definition black_magic (n: nat) (lst: iList n) :=
  match lst as y in iList n return if (NPeano.odd (n + sum lst)) then Cat else Dog with
    | _ => match (NPeano.odd (n + sum lst)) as y in bool return if y then Cat else Dog with
                                                                     | true => cat
                                                                     | false => dog
                                                                   end
  end.
                                                                                  

On Tue, Oct 15, 2013 at 10:36 AM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

1) The type of E is fixed, I just needed names to refer to the
concrete instances of the indices in E. So e1 stands for whatever
concrete value the term E has for its first index.

2) It's actually put quite well in Adam's book.

- Valentin

On Mon, Oct 14, 2013 at 9:10 PM, t x <txrev319 AT gmail.com> wrote:
> 1) I was not aware that the _TYPE_ of E could also be different. Previously
> I thought that the type of E was fixed, but the "match type" can depend on
> the value of E. Now, it's clear to that even the type of E is not fixed.
>
> 2) I'm still not convinced I understand dependent type matching (though
> Adam's 4 paragraphs in CPDT is starting to make more sense.)
>
> Is it possible to express "the one rule of dependent type matching" as a
> inference rule, i.e. things like:
>
> Env |- t1: A -> B
> Env |- t2: A
> ------------------------
> Env |- t1 t2 : B
>
>
>
>
> On Mon, Oct 14, 2013 at 3:38 PM, Valentin Robert
> <valentin.robert.42 AT gmail.com> wrote:
>>
>> Rather (assuming we only talk about indices), if:
>>
>> E : T e1 ... en
>>
>> and:
>>
>> T :=
>> | Ci: ... -> T ci_1 ... ci_n
>>
>> Then it is checked that:
>> 1) Bi : U {y is replaced by Ci, xk is replaced by ci_k}
>>
>> And the resulting term has type:
>> 2) FinalType = U {y is replaced by E, xk is replaced by ek}
>>
>> Unless I'm mistaken.
>>
>> - Valentin
>>
>>
>> On Mon, Oct 14, 2013 at 3:11 PM, t x <txrev319 AT gmail.com> wrote:
>> > Valentin: this is helpful, but I'm not quite there yet.
>> >
>> > Adam: I've seen that section of
>> > http://adam.chlipala.net/cpdt/html/MoreDep.html before -- unfortunately,
>> > I
>> > find the prose difficult to understand.
>> >
>> >
>> > Can I think of type checking as follows:
>> >
>> > Suppose have:
>> >
>> > match E as y in (T x1 ... xn) return U with
>> > | C1 z1_1 z1_2 ... z1_m1 => B1
>> > | C2 z2_1 z2_2 ... z2_m2 => B2
>> > ...
>> > | Ci  zi_1 zi_2 ... zi_mi => Bi
>> > ...
>> > end : FinalType
>> >
>> > then to have a valid type check, we need the following properties:
>> >
>> > 1) forall i, (E = Ci zi_1 ... zi_mi) ->
>> >   type_of ( Bi ) =  U { y replaced with Ci zi_1 ... zi_mi}
>> >
>> > 2) there needs to be some relation between U and FinalType -- but I
>> > think
>> > it's more subtle than "U = FinalType"
>> >
>> >
>> >
>> >
>> >
>> > On Mon, Oct 14, 2013 at 2:52 PM, Adam Chlipala <adamc AT csail.mit.edu>
>> > wrote:
>> >>
>> >> Section 8.2, "The One Rule of Dependent Pattern Matching in Coq," in
>> >> CPDT
>> >> <http://adam.chlipala.net/cpdt/> might clear this up.  There really is
>> >> a
>> >> pretty straightforward typing rule behind this behavior and that of all
>> >> [match]es in Coq.
>> >>
>> >>
>> >> On 10/14/2013 05:35 PM, t x wrote:
>> >>>
>> >>> 1) eq_rect =
>> >>> 2)  fun (A: Type) (x: A) (P: A -> Type) (f: P x) (y: A) (e : @eq A x
>> >>> y)
>> >>> =>
>> >>> 3)    match e in (@eq _ _ y0) return (P y0) with
>> >>> 4)      | eq_refl => f
>> >>> 5)    end :
>> >>> 6)      forall (A: Type) (x: A) (P: A -> Type),
>> >>> 7)        P x -> forall y : A, @eq A x y -> P y
>> >>>
>> >>> 8) Inductive eq (A: Type) (x: A) : A -> Prop := refl-equal : eq A x x.
>> >>>
>> >>> I'm reading Chapter 8 of Coq d'Art, and trying to better understand
>> >>> eq.
>> >>>
>> >>> "equality" has been interesting in that (1) there were many "obviously
>> >>> equal" things that Coq did not agree with me on and (2) I still don't
>> >>> understand how Coq's equality works.
>> >>>
>> >>> The above definition -- especially line 3, seems a bit magical to me:
>> >>>
>> >>> a)  we say "match e in (@eq _ _ y0)" -- so y0 must be bound to y
>> >>> b)  then we say "return (P y0)", which means "return (P y)"
>> >>> c)  but then we return f, which has type "(P x)"
>> >>>
>> >>> and Coq is happy and fine with this. I'm not happy with this. What is
>> >>> Coq
>> >>> doing to convert the "(P x)" to a "(P y)" and why is it allowed in
>> >>> this
>> >>> case?
>> >
>> >
>
>