Changeset 2108 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (7 years ago)
Author:
mulligan
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2101 r2108  
    604604qed.
    605605
    606 axiom eq_identifier_eq:
     606axiom eqb_succ_injective_Pos:
     607  ∀l, r: Pos.
     608    eqb (succ l) (succ r) = true → eqb l r = true.
     609
     610lemma eqb_true_to_refl_Pos:
     611  ∀l, r: Pos.
     612    eqb l r = true → l = r.
     613  #l #r @(pos_elim2 … l r)
     614  [1:
     615    #r cases r
     616    [1:
     617      #_ %
     618    |2,3:
     619      #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
     620    ]
     621  |2:
     622    #l cases l
     623    [1:
     624      normalize in ⊢ (% → ?); #absurd destruct(absurd)
     625    |2,3:
     626      #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)
     627    ]
     628  |3:
     629    #l #r #inductive_hypothesis #relevant @eq_f
     630    @inductive_hypothesis @eqb_succ_injective_Pos
     631    assumption
     632  ]
     633qed.
     634
     635lemma eq_identifier_eq:
    607636  ∀tag: String.
    608637  ∀l.
    609638  ∀r.
    610639    eq_identifier tag l r = true → l = r.
     640  #tag #l #r cases l cases r
     641  #pos_l #pos_r
     642  cases pos_l cases pos_r
     643  [1:
     644    #_ %
     645  |2,3,4,7:
     646    #p1_l normalize in ⊢ (% → ?);
     647    #absurd destruct(absurd)
     648  |5,9:
     649    #p1_l #p1_r normalize in ⊢ (% → ?);
     650    #relevant
     651    >(eqb_true_to_refl_Pos … relevant) %
     652  |*:
     653    #p_l #p_r normalize in ⊢ (% → ?);
     654    #absurd destruct(absurd)
     655  ]
     656qed.
    611657
    612658axiom neq_identifier_neq:
     
    614660  ∀l, r: identifier tag.
    615661    eq_identifier tag l r = false → (l = r → False).
    616 
     662 
    617663(* label_map: identifier ↦ pseudo program counter *)
    618664definition label_map ≝ identifier_map ASMTag ℕ.
Note: See TracChangeset for help on using the changeset viewer.