Next: Induction Up: New features in LEGO Version 1.3 Previous: Configure Equality

# LEGO Version 1.3: Elimination Rule for Relations

Consider inductive families defined with Relation, typically:

```  Inductive [R:T1->..->Tn->UNIV] Relation
Constructors
[rule1 : {x1:t1}..{xk:tk} (* schematic variables *)

(* inductive premises *)
(R p1 .. pn)->..->(R p'1 .. p'n)->       (* side conditions *)
(*--------------------------------------*) S1->..->Sn->
R c1 .. cn
(* conclusion *)                               ]
(* more rules *)
[ruleN: (* same pattern *) ];
```

Previously, the elimination rule generated and assumed was

```  R_elim : {C_R:T1->..->Tn->UNIV} (* C_R does not depend on proofs of R *)
({x1:t1}..{xk:tk}S1->..->Sn-> (* rule1 case *)
(C_R p1 .. pn)->..->(C_R p'1 .. p'n)->C_R c1 .. cn)->
(* more cases *)
{a1:T1}..{an:Tn}(R a1 .. an)->C_R a1 .. an
```

This captured directly the idea that R is the smallest relation satisfying its rules.

However, observe that in each case, we get (C_R p1 .. pn) etc as hypotheses, but not the (R p1 .. pn) etc themselves, often very useful. We can add these hypotheses for a given

```  C_R = [b1:T1]..[bn:Tn]P
```

by replacing it with

```  C_R = [b1:T1]..[bn:Tn]and (R b1 .. bn) P
```

and reconstructing explicitly the proof of (R b1 .. bn) we morally already have.

In the light of this, and since it is easier to ignore useless hypotheses than to reconstruct useful ones, we now add them in when we generate the elimination rule, which now looks like this:

```  R_elim : {C_R:T1->..->Tn->UNIV} (* C_R does not depend on proofs of R *)
({x1:t1}..{xk:tk}S1->..->Sn-> (* rule1 case *)
(R p1 .. pn)->..->(R p'1 .. p'n)->
(C_R p1 .. pn)->..->(C_R p'1 .. p'n)->C_R c1 .. cn)->
(* more cases *)
{a1:T1}..{an:Tn}(R a1 .. an)->C_R a1 .. an
```

This formulation is no stronger than the previous one, but hopefully more convenient.