How to write a type-safe unwrap (aka fromJust)

Posted by Clément Pit-Claudel on Fri 19 June 2020 in Coq. Tagged with dependent-types, tricks.

Tips and tricks for writing functions that take proofs as arguments.

Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (UntypedAST) and one for typed terms (TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!

typecheck
     : UntypedAST -> option TypedAST
interp
     : TypedAST -> Value

You write a few programs…

Example well_typed := UAdd (UNat 1) (UNat 1).
Example ill_typed := UAdd (UNat 1) (UBool true).

… typecheck them:

Definition tc_good := typecheck well_typed.

= Some
    {|
    tau := Nat;
    ast := TAdd (TNat 1) (TNat 1) |}
: option TypedAST


Definition tc_bad := typecheck ill_typed.

= None
: option TypedAST

… and attempt to run them:

The term "tc_good" has type "option TypedAST"
while it is expected to have type "TypedAST".

D'oh! interp takes a TypedAST, but typecheck returns an option. What do we do?


Continue reading

Computing with opaque proofs

Posted by Clément Pit-Claudel on Wed 17 June 2020 in Coq. Tagged with dependent-types, tricks.

Computations with dependent types often get stuck on rewrites that use opaque lemmas. When the corresponding equality is decidable, these lemmas don't need to be made transparent to unblock computation.

A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:

Import EqNotations Vector.VectorNotations.

= match
    match
      Nat.add_1_r 3 in (_ = H)
      return (Vector.t nat H)
    with
    | eq_refl => [1; 2; 3; 4]
    end as c in (Vector.t _ H)
    return
      (match
         H as c0 return (Vector.t nat c0 -> Type)
       with
       | 0 =>
           fun _ : Vector.t nat 0 =>
           False -> forall x1 : Prop, x1 -> x1
       | S x => fun _ : Vector.t nat (S x) => nat
       end c)
  with
  | [] =>
      fun x : False =>
      match
        x return (forall x0 : Prop, x0 -> x0)
      with
      end
  | h :: _ => h
  end
: (fun (n : nat) (_ : Vector.t nat (S n)) => nat)
    3
    (rew [Vector.t nat] Nat.add_1_r 3 in
     ([1; 2; 3] ++ [4]))

This post shows how to work around this issue.


Continue reading