The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  I updated the test-suite file of Equations (https://github.com/mattam82/Coq-Equations) 

that makes this go through entirely automatically (modulo a permutation of arguments 

that shouldn't be necessary) and simplifies the proof drastically using functional elimination.

To anyone who would like to try, note that Equations (branch 8.5) compiles only with the 

current 8.5 branch of Coq, not the beta1. It boils down to:

<<<

Require Import Equations.

(** Hints for automatically solving recursive call obligations *)

Lemma size_ii_open_rec_lt :

  forall (i : index) (x : fvar),

    index_size (ii_open_var i x) < S (index_size i).

Proof.

  intros; unfold ii_open_var; rewrite size_ii_open_rec. auto with arith.

Defined.

Hint Extern 3 => progress cbn : Below.

Hint Resolve size_ii_open_rec_lt : Below.

Hint Extern 3 => progress auto with arith : Below.

Equations infer_sort (i : index)  (ie : env) : option sort :=

infer_sort i ie by rec i (MR lt index_size) :=

infer_sort (IBVar x) ie := None ;

infer_sort (IFVar x) ie := get x ie;

infer_sort Z ie := Some N;

infer_sort (Plus1 i) ie <= infer_sort i ie => {

                     | Some N := Some N;

                     | _ := None };

infer_sort (IAbs s i) ie <= let x := (var_gen (dom ie \u ifv i)) in 

                            infer_sort (ii_open_var i x)  ((x, s) :: ie)  => {

  infer_sort (IAbs s i) ie (Some s2) := Some (ArrowS s s2) ;

  infer_sort _ _ _ := None } ;

infer_sort (IApp i1 i2) ie <= infer_sort i1 ie => {

infer_sort (IApp i1 i2) ie (Some (ArrowS s1 s2)) 

     <= infer_sort i2 ie =>

      { | None := None;

        | Some s1' <= eq_sort_dec s1 s1' => {

                   | (left _) := Some s2;

                   | (right _) := None } };

infer_sort (IApp i1 i2) ie _ := None }.

Lemma infer_sort_sound: 

  forall (i : index) (ie: env)  (s : sort),

    infer_sort i ie = Some s -> 

    sorting ie i s.

Proof.

  intros i ie. funelim (infer_sort i ie); intros s' Heqs; 

               try (noconf Heqs || (rewrite Heq in Heqs; noconf Heqs)).

  - now constructor. 

  - subst s'. now constructor.

  - subst s'. specialize (Hind _ Heq). now constructor.

  - subst s'. specialize (Hind _ Heq). now constructor.  

  - subst s0. pose proof (Hind _ Heq0). pose proof (Hind0 _ Heq1).

    econstructor; eauto.

Qed.

>>>

Best,

-- Matthieu

2015-04-02 10:31 GMT+02:00 Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>:

Just for the sake of completeness, I updated the gist file in order to work for abstraction case as well.

https://gist.github.com/zoep/6167e14ed0ebe0887a03

Cheers,

Zoe