The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Aha, it's non-trivial indeed but you can do the unfolding trick. Maybe
you didn't get the right induction hypothesis because you need to redo
the well-founded induction in the lemma, and also generalize by the ie
variable.

The tricky part is setting up the unfolding lemma such that
you don't get into huge terms. Note that this is assuming functional
extensionality.

Definition infer_sort_unfold (ie : env) (i : index) : option sort :=
  match i with
    | IBVar x => None
    | IFVar x => get x ie
    | Z => Some N
    | Plus1 i =>
      match infer_sort ie i with
        | Some N => Some N
        | _ => None
      end
    | IAbs s i =>
      (* let x := var_gen (dom ie \u ifv i) in *)
      let x := 3 in (* Just for the example *)
      match infer_sort ((x, s) :: ie) (ii_open_var i x) with
        | Some s' => Some (ArrowS s s')
        | _ => None
      end
    | IApp i1 i2 =>
      match infer_sort ie i1 with
        | Some (ArrowS s1 s2) =>
          match infer_sort ie i2 with
            | Some s1' =>
              if sort_eq_dec s1 s1' then Some s2
              else None
            | _ => None
          end
        | _ => None
      end
  end.

Import WfExtensionality.

Program Lemma fix_sub_eq_ext :
  forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
         (P : A -> Type)
         (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x)
         f (Heq : f = Fix_sub A R Rwf P F_sub),
  forall x : A, Fix_sub A R Rwf P F_sub x = F_sub x f.
Proof.
  intros. subst f. apply fix_sub_eq_ext.
Qed.

Lemma infer_sort_eq ie i : infer_sort ie i = infer_sort_unfold ie i.
Proof.
  unfold infer_sort.
  unfold infer_sort_func.
  rewrite (fix_sub_eq_ext (f:=infer_sort_func) eq_refl). simpl.
  destruct i; try reflexivity.
  fold (infer_sort ie i); simpl.

  destruct (infer_sort ie i) as [[|s1 s2]|]; reflexivity.

  change (infer_sort_func _) with
    (infer_sort ((3, s) :: ie) (ii_open_var i 3)); simpl.
  destruct infer_sort; reflexivity.

  change (infer_sort_func (existT _ ie i1)) with
    (infer_sort ie i1); simpl.
  destruct (infer_sort ie i1). destruct s as [[|s1 s2]|]; try reflexivity.
  fold (infer_sort ie i2). destruct infer_sort; try reflexivity.
  reflexivity.
Qed.

Require Import Wellfounded.
Lemma infer_sort_sound:
  forall (i : index) (ie: env)  (s : sort),
    infer_sort ie i = Some s ->
    sorting ie i s.
Proof.
  change (forall i, (fun i => forall ie s , infer_sort ie i = Some s
-> sorting ie i s) i).
  apply (well_founded_induction_type (R:=MR lt index_size)).
  * unfold MR. apply wf_inverse_image. apply lt_wf.
  * intros i IH ? ?. rewrite infer_sort_eq.
    destruct i; simpl; intros H; try discriminate.
    - now constructor.
    - injection H; intros Hs; subst s. now constructor.
    - revert H. case_eq (infer_sort ie i).
      { intros [|s1 s2].
        + intros Hn Hs; injection Hs; intros <-. constructor. apply 
IH;trivial.
          red; simpl. apply lt_n_Sn.
        + intros Hn Hs; discriminate. }
      intros; discriminate.
    - revert H; case_eq (infer_sort ((3,s0)::ie) (ii_open_var i 3)).
      intros s1 Hinfer. intros Heq; injection Heq; intros <-.
      specialize (IH (ii_open_var i 3) (size_ii_open_rec_lt _ _) _ _ Hinfer).
      admit.
      intros; discriminate.
    - revert H.
      case_eq (infer_sort ie i1); try discriminate.
      intros [s1 s2|]; try discriminate.
      case_eq (infer_sort ie i2); try discriminate.
      intros s' Hi2 s1 s2 Hi1.
      destruct sort_eq_dec; try discriminate.
      subst s1. intros H; injection H; intros <-.
      unfold MR in IH. simpl in IH.
      assert (si1:index_size i1 < S (index_size i1 + index_size i2))
by auto with arith.
      assert (si2:index_size i2 < S (index_size i1 + index_size i2))
by auto with arith.
      pose proof (IH _ si2 _ _ Hi2).
      pose proof (IH _ si1 _ _ Hi1).
      econstructor; eassumption.
Admitted.

-- Matthieu


2015-03-30 16:19 GMT+02:00 Zoe Paraskevopoulou 
<zoe.paraskevopoulou AT gmail.com>:
> Hello,
>
> Thank you all for your answers, I really appreciate your help!
>
> On Mar 30, 2015, at 1:16 AM, Matthieu Sozeau 
> <mattam AT mattam.org>
>  wrote:
>
>   the classic answer is to build an unfolded version (without Program and
> which
> calls the folded version at recursive calls) and show extensional
> equivalence of
> the two definitions, then you can easily control unfolding using rewriting,
> and
> avoid the clutter due to decoration of matches with equalities at matches.
>
>
> With this I had with the same problem with the original proof, I cannot
> handle the inductive case. Further case analysis also does not seem to help.
>
> On Mar 30, 2015, at 1:16 AM, Matthieu Sozeau 
> <mattam AT mattam.org>
>  wrote:
>
> [Function] might help too but I couldn't manage to make
> it work on this example.
>
>
> I also tried (unsuccessfully) make it work with [Function].
>
> On Mar 30, 2015, at 12:31 AM, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> Definition infer_sort':= Eval compute in infer_sort.
>
>
> Unfortunately, this takes way to much time (even with a lazy evaluation
> strategy) so I was not able to see if it is helpful at all.
>
> I think I will go for one of the following:
>
> - The dependent types solution (proposed by Jonathan and James) which seems
> to work fine and I hope it scales to more complex functions and
> specifications.
>
> - I also think that I can completely circumvent the problem (for now) by
> defining everything relationally as inductive definitions (I won’t need
> sort_infer for this).
>
> - Switch to plain De Bruijn indices instead of locally nameless
> representation that will allow me to define such functions with structural
> recursion.
>
> Cheers,
> Zoe
>