Module DependentMatchExamples. (** * Introduction to dependent match *) (** Consider a match expression [[ match e with | C1 => e1 | C2 => e2 | C3 => e3 ... end ]] The usual typing rule for the above is quite simple. First, the match must be exhaustive, i.e., the patterns [C1,C2,C3,...] must cover all the cases. In other words, all the constructors for the type of [e] must be handled. Then, all the branches [e1,e2,e3,...] must be of the same type [T]. When this holds, the whole match expression is typed with type [T]. For instance: *) Definition isZero (n : nat) : bool := match n with | 0 => true | S x => false end . (** Above, we handle both constructors for [nat], namely zero and successor. Also, both branches [true,false] have type [bool], hence the whole match has type [bool], and isZero typechecks. This typing mechanism for [match] is indeed the one used in most functional programming languages. When proving theorems via the Curry-Howard isomorphism, e.g. in Coq, the above match typing rule is sometimes overly restrictive. Consider for instance: [[ Definition foo (P : nat -> Prop) (H0 : P 0) (HS : forall n, P (S n)) (x : nat) : P x := ... ]] Intuitively, here [P] is a predicate on [nat], and we need to prove [P x] for any [x]. We have as hypotheses, that [P] holds on [0] and [S n] for any [n], so the proof should be a simple case analysis on [x]. We get: [[ Definition foo (P : nat -> Prop) (H0 : P 0) (HS : forall n, P (S n)) (x : nat) : P x := match x with | 0 => H0 | S n => HS n end ]] The above definition is very reasonable but it can _not_ be typed using the match typing rule seen before! In fact, the first branch [H0] has type [P 0] while the second branch has type [P (S n)]. Of course, one might object that in the first branch [x] is [0], while il the second [x] is [S n], so both branches intuitively _should_ be assigned the common type [P x] instead. This however requires a more sophisticated typing mechanism known as the "dependent match" typing. *) (* *) (**********************************************************) (** * Dependence on the _value_ of the term being matched *) (** We shall use a simple color type, containing only two colors. *) Inductive color : Set := white | black . (** ** Simple example for [match .. as ..] *) (** Consider the definition below: *) Definition match_as_0 (P : color -> Prop) (Hw : P white) (Hb : P black) (f : color -> color) : P (f white) := match f white with | white => Hw (* : P white *) | black => Hb (* : P black *) end . (** Coq accepts the above match. Why? The two branches have different types, namely [P white] and [P black], violating the rule for match typing! The return type of [match_as_0] is [P (f white)] which is even different from both! On further inspection, the definition is at least morally correct. For instance the first branch returns [Hw] which is of type [P white] instead of the claimed [P (f white)]. This may look wrong, but we reach this branch only when [f white] is [white], so there is no real difference between the expected and actual types. Similarly, the second branch is reached only when [f white] is [black], so [Hb] of type [P black] can be thought to have type [P (f white)] as well. Intuitive reasons aside, how did Coq manage to type check the above match? Curiously, if we inspect the definition, we notice that Coq has added something to our code. *) Print match_as_0. (* Reported below. *) Definition match_as_0_fixed_by_Coq := fun (P : color -> Prop) (Hw : P white) (Hb : P black) (f : color -> color) => match f white as x return (P x) with | white => Hw | black => Hb end . (** Notice the extra [as x return (P x)] part. This special match is used to state that the type of the whole match expression depends on the value of the term being matched [f white]. That is, the type of the match is [P x], where [x] is [f white]. In other words, it is [P (f white)] which is what we need. What about type checking the branches? The idea is that when checking [[ | white => Hw ]] we require that [Hw] has type [P x] where [x] is the value _we are matching against_, that is, [white]. So, [Hw] is checked against [P white]. Similarly, [[ | black => Hb ]] makes [Hb] to be checked against [P x] where [x] is [black], hence against [P black]. This form of match is called a "dependent match", indicating that the type for the whole match expression is dependent on the term being matched. Rough summary: - The type for a match expression can be expressed as a function of the term being matched; - The branches [C => e] are then checked by applying said function to [C], hence obtaining a type, and then checking [e] against that. Note that if the type-valued function is constant, as in [[ match e as x return nat with ... ]] we get all the branches checked against nat. That is, we recover the typing of the non-dependent match. This shows that the regular match is indeed a special case of the dependent match. As a final remark, note that in the above case Coq was able to guess the function which related the value of the term being matched and the target type. Coq has some heuristics to help the user in this task. In the general case, however, the user has to define explicitly the function, annotating the dependent matches with [as x return ...] . *) (* *) (***************************************************************************) (** * Dependent match: dependence on the _type_ of the term being matched *) (** ** Simple example for [match ... in ...] *) (** This is a simple predicate on colors, which holds only on black *) Inductive isBlack : color -> Prop := | B : isBlack black . (** Consider this Coq definition, which does not pass type checking. [[ Definition match_in_0 (P : color -> Prop) (H : P black) (x : color) (H2 : isBlack x) : P x := H . ]] The above definition fails with <> However, the above [Definition] is morally right. The [match_in_0] function above takes as an argument [H2 : isBlack x], so we know that [x] is actually [black]. Hence, the type error above complaining about the difference between [P black] and [P x] is just due to the type checker being overly restrictive here. How can we convince the type checker to accept the definition above? Let's try by matching over [H2] which claims [x] is [black]. *) Definition match_in_0 (P : color -> Prop) (H : P black) (x : color) (H2 : isBlack x) : P x := match H2 with | B => H end . (** Note the strange typing here: [[ H : P black match H2 with B => H end : P x ]] The match intuitively returns the same value as [H], yet inside a different type. We know this is OK since [x] must be black for [H2] to exist, but why this match is allowed by Coq? Inspecting the [match_in_0 term], we discover that Coq added something to our definition! *) Print match_in_0. Definition match_in_0_fixed_by_Coq := fun (P : color -> Prop) (H : P black) (x : color) (H2 : isBlack x) => match H2 in (isBlack c) return (P c) with | B => H end . (** Note the extra [in (isBlack c) return (P c)] part. This is stating that the whole match expression has type [P c] where [c] is the color for which we have [H2 : isBlack c]. This means that [c] is [x], hence the whole match has type [P x]. However, when [in .. return ..] is specified for a match, the typing of the match branches is done differently. Typing the branch [[ | B => H ]] no longer requires [H] to have type [P x] as the whole match expression. Instead, [H] has to have type [P c] where [c] is the color for which we have [B : isBlack c]. Of course, we have [B : isBlack black], so [c] is [black], hence [P c] is [P black]. Rough summary: - The type of "match A" can be expressed as a function of the type of A; - Checking a branch "C => e" is done by applying said function to the type of the constructor C, and then checking e against this type. Note that in out example above Coq was able to guess how to express the match type [P x] as a function of type of the matched term [isBlack x]. In the general case, however, Coq will not be able to define the function and the user has to provide it. This more sophisticated form of match is called a "dependent match". Here, the adjective "dependent" means that the returned type depends of the type of the object being matched. As a final remark, consider the case in which the function is constant, e.g, [[ match H2 in isBlack c return nat with ... ]] In this case, every branch is checked to have type nat, and the whole match will have type nat. This shows that once again a regular match is just a special case of the dependent match of the [in..return..] variant. *) (** ** Advanced example for [match .. in ..] *) (** Let's define a relation holding between opposite colors. *) Inductive opposite : color -> color -> Prop := | WB : opposite white black | BW : opposite black white . (** The following definition is morally correct but is not accepted by Coq. [[ Definition match_in_1 (P : color -> Prop) (H : P black) (x : color) (H2: opposite white x) : P x := H . ]] Coq complains with <> While types [P black] and [P x] are syntactically different, the function above takes as an argument [H2 : opposite white x], and this implies that [x] is actually [black], so that the distinction between [P black] and [P x] is not a real one. Adapting the code above to pass the type checker is non trivial. *) Definition match_in_1 (P : color -> Prop) (H : P black) (x : color) (H2: opposite white x) : P x := let f (a b : color) : Prop := match a with | white => P b | black => True end in match H2 in opposite a b return f a b with | WB => H (* : f true false == P false *) | BW => I (* : f false true == True *) end (* : f true x == P x *) . (** The above example intuitively transformed a [P black] value into a [P x] value, when we had a proof implying that [x] was [black]. The next example shows instead how to convert a [P x] into a [P black], when holding the same proof. Surprisingly, this requires a bit more finesse. *) Definition match_in_2 (P : color -> Prop) (x : color) (H : P x) (H2: opposite white x) : P black := let f (a b : color) : Prop := match a with | white => (P b -> P black) (* An implication! *) | black => True end in match H2 in opposite a b return f a b with | WB => fun H3 => H3 (* f white black == P black -> P black *) | BW => I (* f black white == True *) end (* f white x == P x -> P black *) H (* Apply the match to H : P x *) . End DependentMatchExamples.