[fix] and [cofix] should be multigoal to avoid repetition

[mattam82]

Description of the problem

The [fix] and [cofix] tactics should have a multigoal variant (or be multigoal), typicall use case is when proving mutual induction principles:

Goal (forall t1, ind1 t1 -> P t1) /\ (forall t2, ind2 t2 -> P t2).
  split. 
  (* Here we have two goals that can be solved together using mutual recursion: 

  forall t : term, id_term_ind t (id_term t)

subgoal 2 (ID 79) is:
 forall t : term_list, id_term_ind_1 t (id_tlist t)
*)
  We need to use [fix] twice to solve them instead of just once.

[herbelin]

@mattam82: could you give more context? I don't see the problem.

[mattam82]

I want an all:fix i_n ... i_k that applies to k subgoals and does mutual recursion on the i_k's arguments to solve all the subgoals at once. Note only do I have to duplicate the calls to fix in each subgoal, they are also different calls to fix, as e.g the second goal here is a fix on term_list not term

[mattam82]

@herbelin Do you agree with the idea? If so, I think I'll get to it soon, I just need that to prove mutual induction theorems in a simple way. In a way, it looks like it could replace the current Lemma .. with .. implementation, with the only difference being that [fix i_n .. i_k] needs to know the recursive arguments right away.

[herbelin]

To be honest, I could not figure out in my mind what was the problem that you have. Is that that you'd like some syntax for

all:[> fix id1 1 with (id2 (t : term_list) {struct t} : id_term_ind_1 t (id_tlist t))|
       fix id2 1 with (id1 (t : term) {struct t} : id_term_ind t)]`?)

? In any case, feel free to do what you want.

Not knowing the recursive argument right away is convenient but indeed a bit hackish to implement because the fix is expecting an effective value so I had to give a dummy one, and update it at the time of closing the proof.

Note that Theorem with has still this problem that if you use rewriting without paying enough attention, the guard may refuse the proof. I believe the guard should be improved here wrt such (anodyne) commutative cuts.

[mattam82]

I wrote a prototype starting from the implementation of fix, with it you can do:

Inductive term : Set :=
| Var (n : nat)
| App (t : term) (l : term_list)

with term_list : Set :=
| nilt : term_list
| const : term -> term_list -> term_list.

Fixpoint id_term (t : term) : term :=
  match t with
    Var n => Var n
  | App t l => App (id_term t) (id_tlist l)
  end
with id_tlist (t : term_list) : term_list :=
       match t with
       | nilt => nilt
       | const t tl => const (id_term t) (id_tlist tl)
       end.

Inductive id_term_ind : term -> term -> Prop :=
    id_term_ind_refinement_1 : forall n : nat, id_term_ind (Var n) (Var n)
  | id_term_ind_refinement_2 : forall (t : term) (l : term_list),
                               id_term_ind t (id_term t) ->
                               id_term_ind_1 l (id_tlist l) ->
                               id_term_ind (App t l) (App (id_term t) (id_tlist l))
  with id_term_ind_1 : term_list -> term_list -> Prop :=
    id_term_ind_1_refinement_1 : id_term_ind_1 nilt nilt
  | id_term_ind_1_refinement_2 : forall (t : term) (t0 : term_list),
                                 id_term_ind t (id_term t) ->
                                 id_term_ind_1 t0 (id_tlist t0) ->
                                 id_term_ind_1 (const t t0) (const (id_term t) (id_tlist t0)).

Lemma mutual : (forall t : term, id_term_ind t (id_term t)) /\ (forall t : term_list, id_term_ind_1 t (id_tlist t)).
Proof.
  split.
  all:mfix 1 1.

Note that you don't need to give any type annotation here, everything gets inferred from the goals. The resulting subgoals are:

2 subgoals (ID 5)

  fix_0 : forall t : term, id_term_ind t (id_term t)
  fix_1 : forall t : term_list, id_term_ind_1 t (id_tlist t)
  ============================
  forall t : term, id_term_ind t (id_term t)

subgoal 2 (ID 6) is:
 forall t : term_list, id_term_ind_1 t (id_tlist t)

[herbelin]

Very nice. Do you have also in mind to support taking names, like e.g. mfix t t, and/or a version where you can name the recursive calls, like e.g mfix on t as fix_0, on t as fix_1, or whatever similar syntax?

[SkySkimmer]

@mattam82

I wrote a prototype starting from the implementation of fix, with it you can do:

What happened to the prototype? Is it on a public branch?