Ignore:
Timestamp:
Dec 1, 2010, 6:03:45 PM (9 years ago)
Author:
mulligan
Message:

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vector.ma

    r350 r352  
    139139         match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
    140140          [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    141 //; ndestruct; //.
     141// [ ndestruct | nlapply (S_inj … K); //]
    142142nqed.
    143143
     
    148148  | Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉
    149149  ] (? : S ? = S ?).
    150 //; ndestruct; //.
     150// [ ndestruct | nlapply (S_inj … K); //]
    151151nqed.
    152152
     
    181181        ]
    182182    ]) (refl ? n).
    183  ndestruct; //.
     183##[##1,2: ndestruct | ##3,4: nlapply (S_inj … prf); // ]
    184184nqed.
    185185 
     
    219219          ndestruct(e);
    220220          ##
    221         | ndestruct(e);
     221        | nlapply (S_inj … e); #H; nrewrite > H;
    222222          napply tl'
    223223          ##
     
    397397          ]
    398398    ]) (refl ? n).
    399     ##[##1, 3:
    400         ndestruct (absd);
    401         ndestruct (prf);
    402         napply tl';
    403     ##|##2:
    404         ndestruct (absd);
    405     ##]
     399    ##[##1,2: ndestruct
     400      | nlapply (S_inj … prf); #X; nrewrite < X;
     401        napply tl' ]
    406402nqed.
    407403   
Note: See TracChangeset for help on using the changeset viewer.