Changeset 352


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.

Location:
Deliverables/D4.1/Matita
Files:
7 edited

Legend:

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

    r268 r352  
    3030        ]
    3131    ]) (refl ? n).
    32     ndestruct; //.
     32 ##[##1,2: ndestruct |##*: napply S_inj; //]
    3333nqed.
    3434
     
    5858                | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
    5959                ]
    60             | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)
     60            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (Cons ? o hd tl) a)
    6161            ] (refl ? (S o))
    6262    ]).
    6363    ##[ ndestruct;
    64     ##| ndestruct; @;
    65     ##| ndestruct; @;
    66     ##| ndestruct; @;
    67     ##| ndestruct; @;
    68     ##| #H; nassumption;
    69     ##]
     64    ##|##*: napply S_inj; // ]
    7065nqed.
    7166
     67(*
    7268nlemma insert_lookup_stub:
    7369  ∀A: Type[0].
     
    8480  @.
    8581nqed.
    86 
     82*)
    8783(*
    8884nlemma test:
  • Deliverables/D4.1/Matita/List.ma

    r350 r352  
    236236    ##|##3:
    237237        nnormalize in prf;
    238         ndestruct (prf);
    239         nassumption;
     238        nlapply (S_inj … prf);
     239        #X; nrewrite > X; @;
    240240    ##]
    241241nqed.
  • Deliverables/D4.1/Matita/Nat.ma

    r351 r352  
    1313  Z: Nat
    1414| S: Nat → Nat.
     15
     16ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m.
     17 #n m H;
     18 nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]);
     19 napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]);
     20 nnormalize; /3/.
     21nqed.
    1522
    1623(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    606613 #m; nelim m; nnormalize
    607614  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
    608     [ #H; ndestruct | /3/ ] /2/.
     615    [ #H; /2/ | /3/ ]
    609616nqed.
    610617
  • Deliverables/D4.1/Matita/Status.ma

    r351 r352  
    893893 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
    894894  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
    895      [ // | #H K; ninversion K [ #H1; ndestruct; // | #x H1 H2 H3; ndestruct ]##]
     895     [ // | #H K; ninversion K [ #H1; nrewrite < H1; // | #x H1 H2 H3; ndestruct ]##]
    896896##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
    897897     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
  • Deliverables/D4.1/Matita/Test.ma

    r350 r352  
    151151 @.
    152152nqed.
    153 
    154 ndefinition testmem ≝ assembly test.
    155 
    156 nlemma foo: testmem = testmem.
    157  nnormalize; @.
    158 nqed.
    159 
    160 ndefinition teststatus ≝ load testmem initialise_status.
    161 
    162 nlemma goo: teststatus = teststatus.
    163  nnormalize; @.
    164 nqed.
    165 
    166 ndefinition testfinal ≝ execute one teststatus.
    167 
    168 nlemma hoo: (*half_add ? (program_counter teststatus)*)
    169   (bitvector_of_nat sixteen (S Z)) = (bitvector_of_nat sixteen (S Z)).
    170  (*half_add (code_memory teststatus) (program_counter teststatus). *)
    171  nwhd in ⊢ (??%?);
    172 
    173 nlemma hoo: testfinal = testfinal.
    174  nwhd in ⊢ (??%?);
    175  nnormalize; @.
    176 nqed.
  • 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   
  • Deliverables/D4.1/Matita/depends

    r344 r352  
    77Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    88Either.ma Bool.ma Maybe.ma Universes.ma
     9DoTest.ma Test.ma
    910ASM.ma BitVectorTrie.ma Either.ma String.ma
    1011Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1112Char.ma Universes.ma
     13Test.ma Assembly.ma Interpret.ma
    1214Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1315Connectives.ma Plogic/equality.ma
Note: See TracChangeset for help on using the changeset viewer.