Ignore:
Timestamp:
Nov 27, 2012, 5:50:51 PM (8 years ago)
Author:
garnier
Message:

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2468 r2496  
    8585 ∃x. e = Some ? x ∧ f x = Some ? res.
    8686 #A #B #e #res #f cases e normalize nodelta
     87[ 1: #Habsurd destruct (Habsurd)
     88| 2: #a #Heq %{a} @conj >Heq @refl ]
     89qed.
     90
     91lemma res_inversion :
     92  ∀A,B:Type[0].
     93  ∀e:option A.
     94  ∀errmsg.
     95  ∀result:B.
     96  ∀f:A → res B.
     97 match e with
     98 [ None ⇒ Error ? errmsg
     99 | Some x ⇒ f x ] = OK ? result →
     100 ∃x. e = Some ? x ∧ f x = OK ? result.
     101 #A #B #e #errmsg #result #f cases e normalize nodelta
    87102[ 1: #Habsurd destruct (Habsurd)
    88103| 2: #a #Heq %{a} @conj >Heq @refl ]
Note: See TracChangeset for help on using the changeset viewer.