doner_kebab.v

Section S.

Context {A B : Set}.

Context (rel : A -> B -> Prop).


Definition determinism : Type 
  := forall (a : A) (b1 b2 : B), rel a b1 -> rel a b2 -> b1 = b2.

Definition totality : Type
  := forall a : A, { b : B | rel a b }.
(*Notation totality := (forall a : A, { b : B | rel a b }) (only parsing).*)


Definition choice (sem : A -> B) : Prop
  := forall a : A, rel a (sem a).

Definition extension (sem : A -> B) : Prop
  := forall (a : A) (b : B), rel a b -> b = sem a.

Definition decidable (sem : A -> B) : Prop
  := forall (a : A) (b : B), rel a b <-> b = sem a.
  
Lemma dec_impl_ext:
  forall {sem : A -> B}, 
    decidable sem -> extension sem.
Proof. intros sem H. exact (fun a b => proj1 (H a b)). Defined.

Lemma dec_impl_choice:
  forall {sem : A -> B}, 
    decidable sem -> choice sem.
Proof. 
  intros sem H. 
  unfold choice.
  intros a.
  remember (sem a) as b eqn:Hb.
  pose proof (H a b) as H3.
  apply H3.
  assumption.
Defined.


Lemma det_choice_impl_dec 
  {sem}
  (rel_det : determinism)
  (sem_choice : choice sem) : decidable sem.
Proof.
  unfold determinism in rel_det.
  unfold choice in sem_choice.
  intros a b1.
  split; intros H1.
  - pose proof (sem_choice a) as H2.
    remember (sem a) as b2 eqn:Hb2.
    apply (rel_det a). assumption. assumption.
  - rewrite H1. apply sem_choice.
Defined.

Lemma ext_impl_det:
  forall {sem : A -> B}, 
    extension sem -> determinism.
Proof.
  intros sem H.
  unfold extension in H.
  intros a b1 b2 H1 H2.
  apply (H a b1) in H1. apply (H a b2) in H2.
  subst. reflexivity.
Defined.

Lemma dec_impl_det:
  forall {sem : A -> B}, 
    decidable sem -> determinism.
Proof.
  intros sem H__dec. 
  eapply ext_impl_det. 
  exact (dec_impl_ext H__dec).
Defined.


Lemma ext_choice_equiv_dec:
  forall {sem : A -> B}, 
    extension sem /\ choice sem <-> decidable sem.
Proof.
  intros sem.
  split.
  - intros [H__ext H__choice].
    apply (det_choice_impl_dec (ext_impl_det H__ext) H__choice).
  - intros H__dec.
    split.
    + apply dec_impl_ext. assumption.
    + apply dec_impl_choice. assumption.
Defined.
    
    
  


Section SSem.

  Context {sem : A -> B}.

  Variable sem_choice : choice sem. (* forall a : A, rel a (sem a). *) (* choice sem. *)

  Definition wit_from_sem: totality (* (a : A) { b : B | rel a b } *)
    := fun a : A => exist (fun b : B => rel a b) (sem a) (sem_choice a).
    
  
  Lemma sem_rel_dec: determinism -> decidable sem.
  Proof.
    intros rel_det.
    exact (det_choice_impl_dec rel_det sem_choice).
  Defined.
  
End SSem.

(*Arguments sem_rel_dec [sem] sem_choice _.*)


Section SWit.

  Variable rel_total : forall a : A, { b : B | rel a b }. (* totality. *)

  Lemma sem_from_wit: { sem : A -> B | forall a : A, rel a (sem a) }.
  Proof.
    refine (exist 
             (fun sem : A -> B => forall a : A, rel a (sem a))
             (fun a : A => proj1_sig (rel_total a))
             _).
    refine (fun a : A => _).
    refine (match (rel_total a) with
            | exist _ b H1 => proj2_sig (rel_total a)
            end).
  Defined.

  Definition sem (a : A) : B := proj1_sig sem_from_wit a.

  Lemma sem_choice: choice sem.
  Proof.
    unfold choice.
    unfold sem.
    destruct sem_from_wit as [sem' H]. simpl. assumption.
  Defined.
  
  Lemma det_wit_dec: determinism -> { sem : A -> B | decidable sem }.
  Proof.
    intros rel_det.
    destruct sem_from_wit as [ sem sem_choice ].
    exists sem.
    exact (@sem_rel_dec sem sem_choice rel_det).    
  Defined.
  
  Lemma det_sem_dec: determinism -> decidable sem.
  Proof.
    intros det.
    apply (det_choice_impl_dec det sem_choice).
  Defined.
  
End SWit.

End S.
(*Arguments sem_from_wit {A B} rel rel_total.*)

Check sem_from_wit.

Check dec_impl_det.

Check sem_rel_dec.
Check wit_from_sem.

(*
Arguments sem_rel_dec {A B} {rel} {sem} sem_choice _.
Check (sem_rel_dec evl_choice).
Arguments wit_from_sem {A B} {rel} {sem} sem_choice.
Check (wit_from_sem evl_choice).
*)




Module SEval2.

Inductive expr : Set :=
  | ENat : nat -> expr
  | EPlus : expr -> expr -> expr
  | EIf : expr -> expr -> expr -> expr.

Inductive eval : expr -> nat -> Prop :=
  | ev_nat (n : nat) : eval (ENat n) n
  | ev_add (e1 e2 : expr) (n1 n2 : nat) : 
      eval e1 n1 -> eval e2 n2 -> eval (EPlus e1 e2) (n1 + n2)
  | ev_ifF (e1 e2 e3 : expr) (n3 : nat) :
      eval e1 0 -> eval e3 n3 -> eval (EIf e1 e2 e3) n3
  | ev_ifT (e1 e2 e3 : expr) (n2 n1 : nat) :
      eval e1 (S n1) -> eval e2 n2 -> eval (EIf e1 e2 e3) n2.

Fixpoint evl (e : expr) : nat :=
  match e with
  | ENat n => n
  | EPlus e1 e2 => (evl e1) + (evl e2)
  | EIf e1 e2 e3 => 
    match evl e1 with
    | (S n) => evl e2
    | 0     => evl e3
    end
  end.
  
Print choice.
  
Lemma evl_choice: choice eval evl. (* forall e, eval e (evl e) *)
Proof.
  unfold choice.
  intros e.
  induction e.
  - simpl. constructor.
  - simpl. constructor. assumption. assumption.
  - remember (evl e1) as n eqn:Hn.
    destruct n.
    + simpl. rewrite <- Hn. apply ev_ifF. assumption. assumption.
    + simpl. rewrite <- Hn. eapply ev_ifT. exact IHe1. assumption.
Defined.

Check evl_choice.


Definition eval_total: forall e : expr, { n : nat | eval e n }
  := wit_from_sem eval evl_choice.
Check (eval_total : totality eval).

(*
Definition extension (sem : A -> B) : Prop
  := forall (a : A) (b : B), rel a b -> b = sem a.
*)

Lemma evl_extension: extension eval evl.
Proof.
  unfold extension.
  intros e.
  induction e; intros m He; inversion He; subst.
  - simpl. reflexivity.
  - apply IHe1 in H1. apply IHe2 in H3. simpl. subst. reflexivity.
  - simpl. apply IHe1 in H3. rewrite <- H3. apply IHe3 in H4. subst. reflexivity.
  - simpl. apply IHe1 in H3. rewrite <- H3. apply IHe2 in H4. subst. reflexivity.
Defined.

(*
Lemma eval_total: totality eval. (* forall e, { n : nat | eval e n } *)
Proof.
  unfold totality.
  intros e.
  exists (evl e).
  apply evl_choice.
Defined.
*)


Lemma eval_deterministic: determinism eval. 
Proof.
  Check dec_impl_det.
  eapply dec_impl_det.
  apply ext_choice_equiv_dec.
  split.
  - apply evl_extension.
  - apply evl_choice.
Defined.

Compute (determinism eval).

Lemma eval_decidable: decidable eval evl.
Proof.
  apply sem_rel_dec.
  - apply evl_choice.
  - apply eval_deterministic.
Defined.

Compute (decidable eval).






Lemma branch_invariant: 
  forall (e2 e3 : expr) (n : nat),
    eval e2 n -> 
    eval e3 n -> 
      forall e1 : expr, eval (EIf e1 e2 e3) n.
Proof.
  intros e2 e3 n.
  intros H2 H3.
  intros e1.
  apply eval_decidable. simpl.
  destruct (evl e1).
  - apply eval_decidable. assumption.
  - apply eval_decidable. assumption.
Defined.




End SEval2.