Changeset 1972


Ignore:
Timestamp:
May 21, 2012, 10:33:26 AM (5 years ago)
Author:
mulligan
Message:

Simple lemma with strangely complex proof complete.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1966 r1972  
    13111311qed.
    13121312
    1313 lemma destruct_bug_fix:
     1313lemma destruct_bug_fix_1:
    13141314  ∀n: nat.
    13151315    S n = 0 → False.
    13161316  #n #absurd destruct(absurd)
     1317qed.
     1318
     1319lemma destruct_bug_fix_2:
     1320  ∀m, n: nat.
     1321    S m = S n → m = n.
     1322  #m #n #refl destruct %
    13171323qed.
    13181324
     
    13241330  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    13251331  [1:
    1326     #absurd @⊥ -b @(destruct_bug_fix 2)
     1332    #absurd @⊥ -b @(destruct_bug_fix_1 2)
    13271333    >absurd %
    13281334  |2:
     
    13301336    cut (n = 2)
    13311337    [1:
     1338      @destruct_bug_fix_2
     1339      >size_refl %
    13321340    |2:
    1333       #n_refl >n_refl in tl;
    1334     cases daemon
     1341      #n_refl >n_refl in tl; #V
     1342      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
     1343      [1:
     1344        #absurd @⊥ -V @(destruct_bug_fix_1 1)
     1345        >absurd %
     1346      |2:
     1347        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
     1348        cut (n' = 1)
     1349        [1:
     1350          @destruct_bug_fix_2 >size_refl' %
     1351        |2:
     1352          #n_refl' >n_refl' in tl'; #V'
     1353          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
     1354          [1:
     1355            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
     1356            >absurd %
     1357          |2:
     1358            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
     1359            cut (n'' = 0)
     1360            [1:
     1361              @destruct_bug_fix_2 >size_refl'' %
     1362            |2:
     1363              #n_refl'' >n_refl'' in tl''; #tl'''
     1364              >(Vector_O … tl''') %
     1365            ]
     1366          ]
     1367        ]
     1368      ]
     1369    ]
    13351370  ]
    1336   cases daemon
    13371371qed.
    13381372
Note: See TracChangeset for help on using the changeset viewer.