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/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:
Note: See TracChangeset for help on using the changeset viewer.