The Coq mailing list

[rcp AT Cs.Nott.AC.UK]

On Mar 12 2007, Adam Chlipala wrote:
> Here's an example for a significantly simpler inversion 
> dilemma that I've encountered.  Advice from others on how to improve 
> this implementation would be very interesting to me!

For those who might be interested in the problem I posed earlier, here is a 
solution, cooked up by the Nottingham team, that computes as desired. I 
hope others may find it useful.


Definition method (n m : nat ) (H : n = m) (P : n = m -> Set) :Set.
     intros n m .
     case  n;  case  m.
     intros. exact (P (refl_equal 0)).   
     intros;  exact unit.  
     intros ; exact unit .
     intros n0 n1 P P1.
     exact (forall H : n1 = n0,  P1 (f_equal S H)).  
Defined. 

Definition no_confusion (n m : nat) (H: n = m) (P : n = m -> Set) : method 
n m H P -> P H.
     intros n m H;  case H.
     case n ; simpl ;  trivial.
     intros;   apply (H0 (refl_equal n0)). 
Defined. 

Definition dep_eq_swap :
 forall (S : Set) ( x y : S) (H: x = y) (P : x = y -> Set ), (forall H' : 
y = x, P (sym_eq H')) -> P H .
  Proof.
     intros S x y H;  case  H.
     intros P H0.
     apply (H0 (refl_equal x)).
Defined .      

Definition finsplit (n m: nat) (i : Fin (n + m)): FinSum n m i.
       intros ;   induction n.
       exact (is_inr i).
       cut (forall (n':nat) (i' : Fin n') ( H : n' = S (n + m)), (eq_rec 
n' Fin i' (S (n + m)) H ) = i -> FinSum (S n) m i) .
       intros ; apply (H (S ( n + m)) i (refl_equal (S (n + m)))); 
trivial.
      intros n0 i'  ;  case i' .
      intros n1 H.
      apply (no_confusion (S n1) (S (n + m)) H (fun H => eq_rec (S n1) Fin 
fz (S (n + m)) H = i ->
           FinSum  (S n) m i) ) ; simpl. 
      intros . 
      clear H.   
     apply (dep_eq_swap nat n1 (n + m) H0 (fun H => eq_rec (S n1) Fin fz 
(S (n + m)) (f_equal S H)
            = i ->  FinSum (S n) m i) ).
    clear H1; clear H0.
    intro H'; case  H';  simpl.
    intro H ;  case H.
    exact (is_inl fz).
    assumption . 
    intros n1 f H.
    apply (no_confusion (S n1) (S (n + m)) H (fun H' => eq_rec (S n1) Fin 
(fs f) (S (n + m)) H' = i ->
           FinSum  (S n) m i) ); simpl.  
    intros. 
    apply (dep_eq_swap nat n1 (n + m) H0 (fun H2 => eq_rec (S n1) Fin(fs 
f) (S (n + m)) (f_equal S H2)
            = i ->  FinSum (S n) m i) ).
    intro H'.
    generalize f;  case H' ; simpl.
    intros f0 H2;  case H2.
    elim (IHn f0).
    exact (fun i0 => is_inl (fs i0)).  
    exact (fun j => is_inr j).   trivial .
Defined.  


Best,

Rawle.



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.