text:
Require Import Setoid.
Require Export refocusing_signatures_cs.
Require Import Wellfounded.Inclusion.
Require Import Wellfounded.Inverse_Image.

Module Lang_Prop (R : RED_LANG_CS) : LANG_PROP R.

  Lemma plug_empty : forall t, R.plug t R.empty = t.
  Proof.
    intros; simpl; auto.
  Qed.
  Hint Resolve plug_empty : prop.

  Lemma compose_empty : forall c : R.context, c = R.compose c R.empty.
  Proof.
    apply app_nil_end.
  Qed.
  Hint Resolve compose_empty : prop.

  Lemma plug_compose : forall (c c' : R.context) (t : R.term), R.plug t (R.compose c c') = R.plug (R.plug t c) c'.
  Proof.
    apply fold_left_app.
  Qed.
  Hint Resolve plug_compose : prop.

End Lang_Prop.

Module RedRefSemCS (R : RED_LANG_CS) (RF : RED_REF_LANG_CS R) <: RED_REF_SEM_CS R.

  Definition dec_term := RF.dec_term.
  Definition dec_context := RF.dec_context.
  Inductive dec : R.term -> R.context -> R.decomp -> Prop :=
  | d_dec  : forall (t : R.term) (c : R.context) (r : R.redex)
               (DT  : dec_term t = R.in_red r),
               dec t c (R.d_red r c)
  | d_v    : forall (t : R.term) (c : R.context) (v : R.value) (d : R.decomp)
               (DT  : dec_term t = R.in_val v)
               (R_C : decctx v c d),
               dec t c d
  | d_term : forall (t t0 : R.term) (c : R.context) (ec : R.elem_context) (d : R.decomp)
               (DT  : dec_term t = R.in_term t0 ec)
               (R_T : dec t0 (ec :: c) d),
               dec t c d
  with decctx : R.value -> R.context -> R.decomp -> Prop :=
  | dc_end  : forall (v : R.value), decctx v R.empty (R.d_val v)
  | dc_dec  : forall (v : R.value) (ec : R.elem_context) (c : R.context) (r : R.redex)
                (DC  : dec_context ec v = R.in_red r),
                decctx v (ec :: c) (R.d_red r c)
  | dc_val  : forall (v v0 : R.value) (ec : R.elem_context) (c : R.context) (d : R.decomp)
                (DC  : dec_context ec v = R.in_val v0)
                (R_C : decctx v0 c d),
                decctx v (ec :: c) d
  | dc_term : forall (v : R.value) (ec ec0 : R.elem_context) (c : R.context) (t : R.term) (d : R.decomp)
                (DC  : dec_context ec v = R.in_term t ec0)
                (R_T : dec t (ec0 :: c) d),
                decctx v (ec :: c) d.

  Scheme dec_Ind := Induction for dec Sort Prop
  with decctx_Ind := Induction for decctx Sort Prop.

  Notation " a <| b " := (RF.subterm_order a b) (at level 40).
  Notation " a <: b " := (RF.ec_order a b) (at level 40).

  Lemma sto_trans : forall t t0 t1, t <| t0 -> t0 <| t1 -> t <| t1.
  Proof with auto.
    induction 2;
    econstructor 2; eauto.
  Qed.

  Lemma plug_le_eq : forall c t t0, R.plug t0 c = t -> t0 <| t \/ (c = R.empty /\ t = t0).
  Proof with auto.
    induction c; intros.
    simpl in H; right; auto.
    left; simpl in H.
    destruct (IHc _ _ H) as [H0 | [H1 H0]]; clear IHc.
    eapply sto_trans; eauto.
    econstructor 1; eauto; econstructor; eauto.
    subst c; econstructor; eauto; econstructor; eauto.
  Qed.

  Lemma st_c : forall t0 t1, t0 <| t1 -> exists c, R.plug t0 c = t1.
  Proof with auto.
    intros; induction H; inversion H; subst.
    exists (ec :: nil); simpl; auto.
    destruct IHclos_trans_n1 as [c H1].
    exists (c ++ (ec :: nil)); unfold R.plug in *; rewrite fold_left_app; simpl; subst; auto.
  Qed.

  Definition value_one_step (v v0 : R.value) : Prop := RF.subterm_one_step (R.value_to_term v) (R.value_to_term v0).
  Definition value_order := clos_trans_n1 R.value value_one_step.

  Notation " a <v| b " := (value_order a b) (at level 40).

  Lemma wf_vo : well_founded value_order.
  Proof.
    apply wf_clos_trans_r; apply wf_inverse_image; apply RF.wf_st1.
  Qed.

(*    Reserved Notation " a <v| b " (at level 40).

    Inductive value_order : R.R.value -> R.R.value -> Prop :=
    | vc_1 : forall v0 v1 ec (ATOM: R.R.atom_plug (R.R.value_to_term v0) ec = (R.R.value_to_term v1)), v0 <v| v1
    | vc_m : forall v0 v1 v2 ec (REC: v0 <v| v1) (ATOM: R.R.atom_plug (R.R.value_to_term v1) ec = (R.R.value_to_term v2)), v0 <v| v2
    where " a <v| b " := (value_order a b).

    Definition hp (v v0 : R.R.value) := (R.R.value_to_term v) <| (R.R.value_to_term v0).

    Lemma wf_vo : well_founded value_order.
    Proof with auto.
      apply wf_incl with hp.
      unfold inclusion; intros; induction H; [ econstructor | econstructor 2]; eauto; econstructor; eauto.
      apply wf_inverse_image; apply R.wf_sto.
    Qed.*)

    Lemma dec_val : forall (v : R.value) (c : R.context) (d : R.decomp), dec (R.value_to_term v) c d -> decctx v c d.
    Proof with eauto.
      induction v using (well_founded_ind wf_vo); intros.
      remember (RF.dec_term (R.value_to_term v)); assert (hh := RF.dec_term_correct (R.value_to_term v));
      destruct i; rewrite <- Heqi in hh.
      symmetry in hh; contradiction (R.value_redex _ _ hh).
      apply R.value_to_term_injective in hh; inversion H0; subst; unfold dec_term in DT;
      rewrite DT in Heqi; inversion Heqi; subst; auto.
      destruct (R.value_trivial v t (e :: nil)); simpl...
      discriminate H1.
      destruct H1 as [v0 H1]; subst t.
      symmetry in hh; assert (ht := RF.st_1 _ _ _ hh);
      apply (tn1_step _ value_one_step) in ht; change (v0 <v| v) in ht.
      inversion H0; subst; unfold dec_term in DT; rewrite DT in Heqi; inversion Heqi; subst.
      clear H0 Heqi DT; assert (H0 := H _ ht _ _ R_T); clear ht R_T.
      generalize dependent v0.
      induction ec using (well_founded_ind RF.wf_eco); intros.
      remember (RF.dec_context ec v0); assert (hc := RF.dec_context_correct ec v0);
      destruct i; rewrite <- Heqi in hc; rewrite <- hh in hc.
      symmetry in hc; contradiction (R.value_redex _ _ hc).
      clear H H0; apply R.value_to_term_injective in hc; subst.
      inversion H1; subst; unfold dec_context in DC; rewrite DC in Heqi; inversion Heqi; subst; auto.
      destruct (R.value_trivial v t (e :: nil)); simpl...
      discriminate.
      destruct H2 as [v1 H2]; subst t.
      inversion H1; subst; unfold dec_context in DC; rewrite DC in Heqi; inversion Heqi; subst.
      clear Heqi H1.
      apply H0 with ec1 v1...
      destruct (RF.dec_context_term_next _ _ _ _ DC)...
      apply H...
      repeat econstructor...
    Qed.

    Lemma val_dec : forall v c d, decctx v c d -> dec (R.value_to_term v) c d.
    Proof with eauto.
      induction v using (well_founded_ind wf_vo); intros.
      remember (RF.dec_term (R.value_to_term v)); assert (hh := RF.dec_term_correct (R.value_to_term v));
      destruct i; rewrite <- Heqi in hh.
      symmetry in hh; contradiction (R.value_redex _ _ hh).
      apply R.value_to_term_injective in hh; subst; econstructor...
      destruct (R.value_trivial v t (e :: nil)); simpl...
      discriminate H1.
      destruct H1 as [v0 H1]; subst t; econstructor 3...
      apply H; [ repeat econstructor | clear Heqi; generalize dependent v0]...
      induction e using (well_founded_ind RF.wf_eco); intros.
      remember (RF.dec_context e v0); assert (hc := RF.dec_context_correct e v0);
      destruct i; rewrite <- Heqi in hc; rewrite hh in hc.
      symmetry in hc; contradiction (R.value_redex _ _ hc).
      clear H H1; apply R.value_to_term_injective in hc; subst; econstructor...
      destruct (R.value_trivial v t (e0 :: nil)); simpl...
      discriminate.
      destruct H2 as [v1 H2]; subst t; econstructor 4...
      apply H.
      repeat econstructor...
      apply H1...
      symmetry in Heqi; destruct (RF.dec_context_term_next _ _ _ _ Heqi)...
    Qed.

  Module RS : RED_SEM_CS R with Definition dec := dec.
    Definition dec := dec.

    Lemma decompose : forall t : R.term, (exists v:R.value, t = R.value_to_term v) \/
      (exists r:R.redex, exists c:R.context, R.plug (R.redex_to_term r) c = t).
    Proof with eauto.
      induction t using (well_founded_ind RF.wf_sto); intros.
      remember (RF.dec_term t); assert (hh := RF.dec_term_correct t); destruct i;
      rewrite <- Heqi in hh.
      right; exists r; exists R.empty...
      left; exists v...
      destruct (H t0) as [[v Hv] | [r [c Hrc]]].
      repeat econstructor...
      subst t0; clear Heqi; generalize dependent v; induction e using (well_founded_ind RF.wf_eco); intros.
      remember (RF.dec_context e v); assert (ht := RF.dec_context_correct e v); destruct i;
      rewrite <- Heqi in ht; rewrite hh in ht.
      right; exists r; exists R.empty...
      left; exists v0...
      destruct (H t0) as [[v0 Hv] | [r [c Hrc]]].
      repeat econstructor...
      symmetry in Heqi; destruct (RF.dec_context_term_next _ _ _ _ Heqi) as [H1 _].
      subst t0; destruct (H0 e0 H1 v0 ht) as [[v1 Hv1] | [r [c Hrc]]].
      left; exists v1...
      right; exists r; exists c...
      right; exists r; exists (c ++ (e0 :: nil));
      subst t0; unfold R.plug in *; rewrite fold_left_app...
      right; exists r; exists (c ++ (e :: nil));
      subst t0; unfold R.plug in *; rewrite fold_left_app...
    Qed.

    Lemma dec_redex_self_e : forall (r : R.redex), dec (R.redex_to_term r) (R.empty) (R.d_red r R.empty).
    Proof with eauto.
      intros; remember (dec_term (R.redex_to_term r)); destruct i; unfold dec_term in Heqi;
      assert (hh := RF.dec_term_correct (R.redex_to_term r)); rewrite <- Heqi in hh; simpl in hh.
      apply R.redex_to_term_injective in hh; subst; constructor...
      contradict hh;  apply R.value_redex.
      symmetry in Heqi; assert (H := RF.dec_term_term_top _ _ _ Heqi).
      econstructor 3; simpl; eauto.
      destruct (R.redex_trivial r t (e :: R.empty) hh) as [H1 | [v H1]]; [ discriminate | subst t].
      clear H Heqi.
      generalize dependent v; generalize dependent e.
      induction e using (well_founded_ind RF.wf_eco); intros.
      apply val_dec.
      remember (RF.dec_context e v); assert (ht := RF.dec_context_correct e v);
      rewrite <- Heqi in ht; destruct i; simpl in ht.
      rewrite hh in ht; apply R.redex_to_term_injective in ht; subst.
      constructor...
      rewrite <- ht in hh; contradiction (R.value_redex _ _ hh).
      econstructor 4; simpl; eauto.
      rewrite hh in ht; destruct (R.redex_trivial r t (e0 :: R.empty) ht) as [H4 | [v1 H4]].
      discriminate.
      subst t; symmetry in Heqi; destruct (RF.dec_context_term_next _ _ _ _ Heqi); apply H...
    Qed.

    Lemma dec_redex_self : forall (r : R.redex) (c : R.context), dec (R.redex_to_term r) c (R.d_red r c).
    Proof with eauto.
      intros.
      assert (hh := dec_redex_self_e r).
      induction hh using dec_Ind with
      (P := fun t c0 d (H : dec t c0 d) => match d with
        | R.d_val v => True
        | R.d_red r' c1 => dec t (R.compose c0 c) (R.d_red r' (R.compose c1 c))
      end)
      (P0:= fun v c0 d (H : decctx v c0 d) => match d with
        | R.d_val v => True
        | R.d_red r' c1 => decctx v (R.compose c0 c) (R.d_red r' (R.compose c1 c))
      end); try destruct d; auto;
      [ constructor | econstructor | econstructor 3 | constructor | econstructor | econstructor 4]...
    Qed.

    Lemma dec_correct : forall t c d, dec t c d -> R.decomp_to_term d = R.plug t c.
    Proof.
      induction 1 using dec_Ind with
      (P := fun t c d (H:dec t c d) => R.decomp_to_term d = R.plug t c)
      (P0:= fun v c d (H:decctx v c d) => R.decomp_to_term d = R.plug (R.value_to_term v) c);
      simpl; auto; match goal with
      | [ DT: (dec_term ?t = ?int) |- _ ] => unfold dec_term in DT; assert (hh := RF.dec_term_correct t); rewrite DT in hh
      | [ DC: (dec_context ?ec ?v = ?int) |- _ ] => unfold dec_context in DC; assert (hh := RF.dec_context_correct ec v); rewrite DC in hh
      end; try rewrite IHdec; rewrite <- hh; subst; auto.
    Qed.

    Lemma dec_plug_rev : forall c c0 t d, dec t (R.compose c c0) d -> dec (R.plug t c) c0 d.
    Proof with auto.
      induction c; intros; simpl; auto.
      apply IHc; clear IHc; remember (RF.dec_term (R.atom_plug t a)); destruct i;
      assert (hh := RF.dec_term_correct (R.atom_plug t a)); rewrite <- Heqi in hh.
      symmetry in Heqi; discriminate ( RF.dec_term_red_empty _ _ Heqi t (a :: nil)); reflexivity.
      symmetry in Heqi; discriminate (RF.dec_term_val_empty _ _ Heqi t (a :: nil))...
      destruct (RF.dec_ec_ord t0 t e a hh) as [H0 | [H0 | [H0 H1]]]; try (subst; econstructor 3; eauto; fail).
      symmetry in Heqi; contradict (RF.dec_term_term_top _ _ _ Heqi _ H0).
      symmetry in hh; destruct (RF.elem_context_det _ _ _ _ H0 hh) as [v H1]; subst t0.
      econstructor 3; eauto.
      clear Heqi; generalize dependent v; generalize dependent e.
      induction e using (well_founded_ind RF.wf_eco); intros.
      apply val_dec.
      remember (RF.dec_context e v); destruct i; symmetry in Heqi;
      assert (ht := RF.dec_context_correct e v); rewrite Heqi in ht.
      contradiction (RF.dec_context_red_bot _ _ _ Heqi a).
      contradiction (RF.dec_context_val_bot _ _ _ Heqi a).
      destruct (RF.dec_context_term_next _ _ _ _ Heqi) as [H2 H3].
      econstructor 4; eauto; rewrite <- hh in ht.
      destruct (RF.dec_ec_ord _ _ _ _ ht) as [H4 | [H4 | [H4 H5]]]; try (subst; auto; fail).
      contradiction (H3 a H1).
      symmetry in ht; clear H3; destruct (RF.elem_context_det _ _ _ _ H4 ht) as [v0 H5]; subst t0.
      apply H0; auto.
    Qed.

    Lemma dec_plug : forall c c0 t d, dec (R.plug t c) c0 d -> dec t (R.compose c c0) d.
    Proof with auto.
      induction c; intros; simpl; auto.
      apply IHc in H; clear IHc; inversion H; subst; unfold dec_term in DT; clear H;
      assert (hh := RF.dec_term_correct (R.atom_plug t a)); rewrite DT in hh.
      discriminate (RF.dec_term_red_empty _ _ DT t (a :: nil)); reflexivity.
      symmetry in hh; discriminate (RF.dec_term_val_empty _ _ DT t (a :: R.empty))...
      destruct (RF.dec_ec_ord t1 t ec a hh) as [H2 | [H2 | [H2 H3]]].
      contradiction (RF.dec_term_term_top _ _ _ DT a).
      symmetry in hh; destruct (RF.elem_context_det _ _ _ _ H2 hh) as [v H3]; subst t1.
      clear DT; generalize dependent v; generalize dependent ec.
      induction ec using (well_founded_ind RF.wf_eco); intros.
      assert (H0 := dec_val _ _ _ R_T); inversion H0; subst; clear R_T;
      assert (ht := RF.dec_context_correct ec v); unfold dec_context in DC; rewrite DC in ht; simpl in ht.
      contradiction (RF.dec_context_red_bot _ _ _ DC a).
      contradiction (RF.dec_context_val_bot _ _ _ DC a).
      clear H0.
      rewrite <- hh in ht.
      destruct (RF.dec_context_term_next _ _ _ _ DC).
      destruct (RF.dec_ec_ord _ _ _ _ ht) as [hq | [hq | [hq hw]]].
      contradiction (H1 a).
      symmetry in ht; destruct (RF.elem_context_det _ _ _ _ hq ht) as [v1 h4]; subst t0.
      apply H with ec1 v1; auto.
      subst; auto.
      subst; auto.
    Qed.

    Inductive decempty : R.term -> R.decomp -> Prop :=
    | d_intro : forall (t : R.term) (d : R.decomp), dec t R.empty d -> decempty t d.

    Inductive iter : R.decomp -> R.value -> Prop :=
    | i_val : forall (v : R.value), iter (R.d_val v) v
    | i_red : forall (r : R.redex) (t : R.term) (c c0 : R.context) (d : R.decomp) (v : R.value),
                R.contract r c = Some (t, c0) -> decempty (R.plug t c0) d -> iter d v -> iter (R.d_red r c) v.

    Inductive eval : R.term -> R.value -> Prop :=
    | e_intro : forall (t : R.term) (d : R.decomp) (v : R.value), decempty t d -> iter d v -> eval t v.

  End RS.

  Definition dec_term_correct := RF.dec_term_correct.
  Definition dec_context_correct := RF.dec_context_correct.

  Lemma dec_val_self : forall v c d, dec (R.value_to_term v) c d <-> decctx v c d.
  Proof.
    split; [apply dec_val | apply val_dec]; auto.
  Qed.

End RedRefSemCS.

Module Red_Prop (R : RED_LANG_CS) (RS : RED_REF_SEM_CS(R)) : RED_PROP R RS.

  Module LP := Lang_Prop R.

  Lemma dec_is_function : forall t d d0, RS.RS.decempty t d -> RS.RS.decempty t d0 -> d = d0.
  Proof.
    intros t d d0 DE DE0; inversion_clear DE; inversion_clear DE0.
    refine (RS.dec_Ind (fun t c d (H:RS.RS.dec t c d) => forall d0 (DEC : RS.RS.dec t c d0), d = d0)
    (fun c v d (H:RS.decctx c v d) => forall d0 (DCTX : RS.decctx c v d0),  d = d0)
    _ _ _ _ _ _ _ t R.empty d DEC d0 DEC0); intros; simpl; auto; try apply H; match goal with
    | [ RD : (RS.RS.dec ?t ?c ?d), DT : (RS.dec_term ?t = ?int) |- _ ] => inversion RD; rewrite DT0 in DT; inversion DT
    | [ RC : (RS.decctx ?v (?ec :: ?c) ?d), DC : (RS.dec_context ?ec ?v = ?int) |- _ ] => inversion RC; rewrite DC0 in DC; inversion DC
    | [ RC : (RS.decctx ?v R.empty ?d) |- _] => inversion RC
    end; subst; auto.
  Qed.
  Hint Resolve dec_is_function : prop.

  Lemma iter_is_function : forall d v v0, RS.RS.iter d v -> RS.RS.iter d v0 -> v = v0.
  Proof with eauto with prop.
    induction 1; intros.
    inversion H...
    inversion H0; subst; rewrite CONTR0 in CONTR; inversion CONTR; subst;
    apply IHiter; cutrewrite (d = d0)...
  Qed.
  Hint Resolve iter_is_function : prop.

  Lemma eval_is_function : forall t v v0, RS.RS.eval t v -> RS.RS.eval t v0 -> v = v0.
  Proof with eauto with prop.
    induction 1; intros; inversion H; subst; cutrewrite (d = d0) in ITER...
  Qed.

  Lemma dec_correct : forall t c d, RS.RS.dec t c d -> R.decomp_to_term d = R.plug t c.
  Proof.
    induction 1 using RS.dec_Ind with
    (P := fun t c d (H:RS.RS.dec t c d) => R.decomp_to_term d = R.plug t c)
    (P0:= fun v c d (H:RS.decctx v c d) => R.decomp_to_term d = R.plug (R.value_to_term v) c); simpl; auto;
    try (assert (hh := RS.dec_term_correct t); rewrite DT in hh; simpl in hh; try rewrite IHdec; subst; auto);
    assert (hh := RS.dec_context_correct ec v); rewrite DC in hh; simpl in hh; try rewrite IHdec; try (contradiction hh); rewrite <- hh; auto.
  Qed.

  Lemma dec_total : forall t, exists d, RS.RS.decempty t d.
  Proof.
    intro t; destruct (RS.RS.decompose t) as [[v Hv] | [r [c Hp]]]; intros; subst t.
    exists (R.d_val v); constructor; rewrite RS.dec_val_self; constructor.
    exists (R.d_red r c); constructor; apply RS.RS.dec_plug_rev;
    rewrite <- LP.compose_empty; apply RS.RS.dec_redex_self.
  Qed.

  Lemma unique_decomposition : forall t:R.term, (exists v:R.value, t = R.value_to_term v) \/
      (exists r:R.redex, exists c:R.context, R.plug (R.redex_to_term r) c = t /\
	  forall (r0:R.redex) c0, (R.plug (R.redex_to_term r0) c0 = t -> r=r0 /\ c= c0)).
  Proof.
    intro t; destruct (RS.RS.decompose t) as [[v H] | [r [c H]]]; intros;
    [left; exists v | right; exists r; exists c]; auto; split; auto; intros.
    assert (RS.RS.decempty t (R.d_red r c)).
    constructor; rewrite <- H; apply RS.RS.dec_plug_rev; rewrite <- LP.compose_empty; apply RS.RS.dec_redex_self.
    assert (RS.RS.decempty t (R.d_red r0 c0)).
    constructor; rewrite <- H0; apply RS.RS.dec_plug_rev; rewrite <- LP.compose_empty; apply RS.RS.dec_redex_self.
    assert (hh := dec_is_function _ _ _ H1 H2); injection hh; intros; auto.
  Qed.

End Red_Prop.
(*
Module RefRedSem_SOS (R : RED_REF_LANG) <: SOS_SEM.

  Definition not_val (t : R.R.term) : Prop := forall v, R.R.value_to_term v <> t.

  Lemma not_triv_term_ec : forall t, ~R.only_trivial t -> exists t0, exists ec0, R.R.atom_plug t0 ec0 = t /\ not_val t0.
  Proof.
    intros; remember (R.dec_term t); destruct i; [contradict H | contradict H | idtac]; symmetry in Heqi.
    unfold R.only_trivial; intros; left; eapply R.dec_term_red_empty; eauto.
    unfold R.only_trivial; intros; left; assert (hh := R.dec_term_correct t);
    rewrite Heqi in hh; subst t; eapply R.value_empty; simpl; eauto.

    assert (hh := R.dec_term_correct t); rewrite Heqi in hh; subst t.

    generalize dependent e; induction e using (well_founded_ind R.wf); intros.

  Definition dec_simpl (t : R.R.term) (H : not_val t) :
    {d : R.R.interm_dec | match d with
      | R.R.in_red r => R.R.redex_to_term r = t
      | R.R.in_val v => False
      | R.R.in_term t0 ec0 => R.R.atom_plug t0 ec0 = t /\ forall v, R.R.value_to_term v <> t0
    end}.
  Proof.
    intros t H; remember (R.dec_term t); destruct i; assert (hh := R.dec_term_correct t); rewrite <- Heqi in hh; simpl in *.
    constructor 1 with (R.R.in_red r);  auto.
    contradiction (H _ hh).
    clear Heqi; generalize dependent e; induction e using (well_founded_ind R.wf).
  *)

Module PreAbstractMachineCS (R : RED_LANG_CS) (RS : RED_REF_SEM_CS (R)) <: PRE_ABSTRACT_MACHINE_CS (R).

  Module LP := Lang_Prop R.

  (** Functions specifying atomic steps of induction on terms and contexts -- needed to avoid explicit induction on terms and contexts in construction of the AM *)
  Definition dec_term : R.term -> R.interm_dec := RS.dec_term.
  Definition dec_context : R.elem_context -> R.value -> R.interm_dec := RS.dec_context.

  Definition dec_term_correct := RS.dec_term_correct.
  Definition dec_context_correct := RS.dec_context_correct.

  Inductive dec : R.term -> R.context -> R.decomp -> Prop :=
  | d_dec  : forall (t : R.term) (c : R.context) (r : R.redex)
                 (DT  : dec_term t = R.in_red r),
                 dec t c (R.d_red r c)
  | d_v    : forall (t : R.term) (c : R.context) (v : R.value) (d : R.decomp)
                 (DT  : dec_term t = R.in_val v)
                 (R_C : decctx v c d),
                 dec t c d
  | d_term : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context) (d : R.decomp)
                 (DT  : dec_term t = R.in_term t0 ec)
                 (R_T : dec t0 (ec :: c) d),
                 dec t c d
  with decctx : R.value -> R.context -> R.decomp -> Prop :=
  | dc_end  : forall (v : R.value), decctx v R.empty (R.d_val v)
  | dc_dec  : forall (v : R.value) (ec : R.elem_context) (c : R.context) (r : R.redex)
                (DC  : dec_context ec v = R.in_red r),
                decctx v (ec :: c) (R.d_red r c)
  | dc_val  : forall (v v0 : R.value) (ec : R.elem_context) (c : R.context) (d : R.decomp)
                (DC  : dec_context ec v = R.in_val v0)
                (R_C : decctx v0 c d),
                decctx v (ec :: c) d
  | dc_term : forall (v : R.value) (ec ec0 : R.elem_context) (c : R.context) (t : R.term) (d : R.decomp)
                (DC  : dec_context ec v = R.in_term t ec0)
                (R_T : dec t (ec0 :: c) d),
                decctx v (ec :: c) d.

  Scheme dec_Ind := Induction for dec Sort Prop
  with decctx_Ind := Induction for decctx Sort Prop.

  Inductive iter : R.decomp -> R.value -> Prop :=
  | i_val : forall (v : R.value), iter (R.d_val v) v
  | i_red : forall (r : R.redex) (t : R.term) (c c0 : R.context) (d : R.decomp) (v : R.value)
              (CONTR  : R.contract r c = Some (t, c0))
              (DEC    : dec t c0 d)
              (R_ITER : iter d v),
              iter (R.d_red r c) v.

  Inductive eval : R.term -> R.value -> Prop :=
  | e_intro : forall (t : R.term) (d : R.decomp) (v : R.value)
                (DEC  : dec t R.empty d)
                (ITER : iter d v),
                eval t v.

  Lemma dec_id_l : forall t c d, RS.RS.dec t c d -> dec t c d.
  Proof with eauto.
    induction 1 using RS.dec_Ind with
    (P := fun t c d (H : RS.RS.dec t c d) => dec t c d)
    (P0:= fun v c d (H0 : RS.decctx v c d) => decctx v c d);
    [ constructor | econstructor 2 | econstructor 3 | constructor | econstructor 2 | econstructor | econstructor 4]...
  Qed.
  Hint Resolve dec_id_l.

  Lemma dec_id_r : forall t c d, dec t c d -> RS.RS.dec t c d.
  Proof with eauto.
    induction 1 using dec_Ind with
    (P := fun t c d (H : dec t c d) => RS.RS.dec t c d)
    (P0:= fun v c d (H0 : decctx v c d) => RS.decctx v c d);
    [ constructor | econstructor 2 | econstructor 3 | constructor | econstructor | econstructor | econstructor 4]...
  Qed.
  Hint Resolve dec_id_r.

  Lemma iterRedPam : forall (d : R.decomp) (v : R.value), RS.RS.iter d v -> iter d v.
  Proof with auto.
    induction 1; [ constructor | constructor 2 with t c0 d; auto;
    inversion_clear D_EM]; rewrite app_nil_end with (l:=c0);
    apply dec_id_l; apply RS.RS.dec_plug...
  Qed.

  Lemma evalRedPam : forall (t : R.term) (v : R.value), RS.RS.eval t v -> eval t v.
  Proof with auto.
    intros t v H; inversion_clear H; constructor 1 with d; [inversion_clear D_EM | apply iterRedPam]...
  Qed.
  Hint Resolve evalRedPam.

  Lemma iterPamRed : forall (d : R.decomp) (v : R.value), iter d v -> RS.RS.iter d v.
  Proof with auto.
    induction 1; [constructor | constructor 2 with t c0 d; auto; constructor];
    apply RS.RS.dec_plug_rev; rewrite <- LP.compose_empty...
  Qed.

  Lemma evalPamRed : forall (t : R.term) (v : R.value), eval t v -> RS.RS.eval t v.
  Proof.
    intros t v H; inversion_clear H; constructor 1 with d; [ constructor | apply iterPamRed]; auto.
  Qed.
  Hint Resolve evalPamRed.

  Theorem evalPam : forall (t : R.term) (v : R.value), RS.RS.eval t v <-> eval t v.
  Proof with auto.
    split...
  Qed.

End PreAbstractMachineCS.

Module StagedAbstractMachineCS (R : RED_LANG_CS) (RS : RED_REF_SEM_CS R) <: STAGED_ABSTRACT_MACHINE_CS R.

  Module PAM := PreAbstractMachineCS R RS.
  Module LP := Lang_Prop R.

  (** Functions specifying atomic steps of induction on terms and contexts -- needed to avoid explicit induction on terms and contexts in construction of the AM *)
  Definition dec_term : R.term -> R.interm_dec := RS.dec_term.
  Definition dec_context : R.elem_context -> R.value -> R.interm_dec := RS.dec_context.

  Definition dec_term_correct := RS.dec_term_correct.
  Definition dec_context_correct := RS.dec_context_correct.

  Inductive dec : R.term -> R.context -> R.value -> Prop :=
  | d_dec  : forall (t : R.term) (c : R.context) (r : R.redex) (v : R.value)
               (DT   : dec_term t = R.in_red r)
               (R_IT : iter (R.d_red r c) v),
               dec t c v
  | d_v    : forall (t : R.term) (c : R.context) (v v0 : R.value)
               (DT   : dec_term t = R.in_val v)
               (R_C  : decctx v c v0),
               dec t c v0
  | d_many : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context) (v : R.value)
               (DT   : dec_term t = R.in_term t0 ec)
               (R_T  : dec t0 (ec :: c) v),
               dec t c v
  with decctx : R.value -> R.context -> R.value -> Prop :=
  | dc_end  : forall (v v0 : R.value)
               (IT_V : iter (R.d_val v) v0),
               decctx v R.empty v0
  | dc_dec  : forall (v v0 : R.value) (ec : R.elem_context) (c : R.context) (r : R.redex)
               (DC   : dec_context ec v = R.in_red r)
               (R_IT : iter (R.d_red r c) v0),
               decctx v (ec :: c) v0
  | dc_val  : forall (v v0 v1 : R.value) (ec : R.elem_context) (c : R.context)
               (DC   : dec_context ec v = R.in_val v0)
               (R_C  : decctx v0 c v1),
               decctx v (ec :: c) v1
  | dc_term : forall (v v0 : R.value) (t : R.term) (ec ec0 : R.elem_context) (c : R.context)
               (DC   : dec_context ec v = R.in_term t ec0)
               (R_T  : dec t (ec0 :: c) v0),
               decctx v (ec :: c) v0
  with iter : R.decomp -> R.value -> Prop :=
  | i_val : forall (v : R.value), iter (R.d_val v) v
  | i_red : forall (r : R.redex) (c c0 : R.context) (t : R.term) (v : R.value)
               (CONTR: R.contract r c = Some (t, c0))
               (R_T  : dec t c0 v),
               iter (R.d_red r c) v.

  Scheme dec_Ind := Induction for dec Sort Prop
  with decctx_Ind := Induction for decctx Sort Prop
  with iter_Ind := Induction for iter Sort Prop.

  Inductive eval : R.term -> R.value -> Prop :=
  | e_intro : forall (t : R.term) (v : R.value), dec t R.empty v -> eval t v.

  Lemma decPamSam : forall (t : R.term) (c : R.context) (d : R.decomp),
    PAM.dec t c d -> forall (v : R.value), iter d v -> dec t c v.
  Proof with eauto.
    induction 1 using PAM.dec_Ind with
    (P := fun t c d (H:PAM.dec t c d) => forall v, iter d v -> dec t c v)
    (P0 := fun c v d (H:PAM.decctx c v d) => forall v', iter d v' -> decctx c v v');
    intros; simpl;
    [econstructor 1 | econstructor 2 | econstructor 3 | constructor | econstructor | econstructor 3 | econstructor 4]...
  Qed.
  Hint Resolve decPamSam.

  Lemma iterPamSam : forall (d : R.decomp) (v : R.value), PAM.iter d v -> iter d v.
  Proof with eauto.
    induction 1; [constructor | econstructor 2]...
  Qed.
  Hint Resolve iterPamSam.

  Lemma evalPamSam : forall (t : R.term) (v : R.value), PAM.eval t v -> eval t v.
  Proof with eauto.
    intros t v H; inversion_clear H; constructor...
  Qed.
  Hint Resolve evalPamSam.

  Module P := Red_Prop R RS.

  Lemma decSamPam : forall (t : R.term) (c : R.context) (v : R.value),
    dec t c v -> forall (d : R.decomp), PAM.dec t c d -> PAM.iter d v.
  Proof with auto.
    induction 1 using dec_Ind with
    (P  := fun t c v (H:dec t c v) => forall d, PAM.dec t c d -> PAM.iter d v)
    (P0 := fun v c v' (H:decctx v c v') => forall d, PAM.decctx v c d -> PAM.iter d v')
    (P1 := fun d v (H:iter d v) => PAM.iter d v); intros; simpl.
    (* Case 1 *)
    change (PAM.dec_term t = R.in_red r) in DT;
    inversion H; rewrite DT0 in DT; inversion DT; subst...
    (* Case 2 *)
    apply IHdec; change (PAM.dec_term t = R.in_val v) in DT;
    inversion H; subst; rewrite DT0 in DT; inversion DT; subst...
    (* Case 3 *)
    apply IHdec; change (PAM.dec_term t = R.in_term t0 ec) in DT;
    inversion H0; subst; rewrite DT0 in DT; inversion DT; subst...
    (* Case 4 *)
    inversion H; subst...
    (* Case 5 *)
    change (PAM.dec_context ec v = R.in_red r) in DC;
    inversion H; subst; rewrite DC0 in DC; inversion DC; subst...
    (* Case 5 *)
    apply IHdec; clear IHdec; change (PAM.dec_context ec v = R.in_val v0) in DC;
    inversion H; rewrite DC0 in DC; inversion DC; subst...
    (* Case 6 *)
    apply IHdec; inversion H0; subst; change (PAM.dec_context ec v = R.in_term t ec0) in DC;
    rewrite DC0 in DC; inversion DC; subst...
    (* Case 5 *)
    constructor.
    (* Case 6 *)
    destruct(P.dec_total (R.plug t c0)) as [d H0]; inversion_clear H0.
    apply RS.RS.dec_plug in DEC; rewrite <- LP.compose_empty in DEC;
    constructor 2 with t c0 d...
  Qed.
  Hint Resolve decSamPam.

  Lemma evalSamPam : forall (t : R.term) (v : R.value), eval t v -> PAM.eval t v.
  Proof with eauto.
    intros t v H; inversion_clear H; destruct (P.dec_total t) as [d H]; inversion_clear H; econstructor...
  Qed.
  Hint Resolve evalSamPam.

  Theorem evalSam : forall (t : R.term) (v : R.value), RS.RS.eval t v <-> eval t v.
  Proof with auto.
    intros t v; rewrite PAM.evalPam; split; intros...
  Qed.

End StagedAbstractMachineCS.

Module EvalApplyMachineCS (R : RED_LANG_CS) (RS : RED_REF_SEM_CS R) <: EVAL_APPLY_MACHINE_CS R.

  Module SAM := StagedAbstractMachineCS R RS.

  Definition dec_term := RS.dec_term.
  Definition dec_context := RS.dec_context.

  Definition dec_term_correct := RS.dec_term_correct.
  Definition dec_context_correct := RS.dec_context_correct.

  Inductive dec : R.term -> R.context -> R.value -> Prop :=
  | d_d_r  : forall (t t0 : R.term) (c c0 : R.context) (r : R.redex) (v : R.value)
               (DT    : dec_term t = R.in_red r)
               (CONTR : R.contract r c = Some (t0, c0))
               (R_T   : dec t0 c0 v),
               dec t c v
  | d_v    : forall (t : R.term) (c : R.context) (v v0 : R.value)
               (DT    : dec_term t = R.in_val v)
               (R_C   : decctx v c v0),
               dec t c v0
  | d_term : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context) (v : R.value)
               (DT    : dec_term t = R.in_term t0 ec)
               (R_T   : dec t0 (ec :: c) v),
               dec t c v
  with decctx : R.value -> R.context -> R.value -> Prop :=
  | dc_end : forall (v : R.value), decctx v R.empty v
  | dc_red : forall (v v0 : R.value) (ec : R.elem_context) (c c0 : R.context) (r : R.redex) (t : R.term)
               (DC    : dec_context ec v = R.in_red r)
               (CONTR : R.contract r c = Some (t, c0))
               (R_T   : dec t c0 v0),
               decctx v (ec :: c) v0
  | dc_rec : forall (v v0 v1 : R.value) (ec : R.elem_context) (c : R.context)
               (DC    : dec_context ec v = R.in_val v0)
               (R_C   : decctx v0 c v1),
               decctx v (ec :: c) v1
  | dc_trm : forall (v v0 : R.value) (ec ec0 : R.elem_context) (c : R.context) (t : R.term)
               (DC    : dec_context ec v = R.in_term t ec0)
               (R_T   : dec t (ec0 :: c) v0),
               decctx v (ec :: c) v0.

  Scheme dec_Ind := Induction for dec Sort Prop
  with decctx_Ind := Induction for decctx Sort Prop.

  Inductive eval : R.term -> R.value -> Prop :=
  | e_intro : forall (t : R.term) (v : R.value), dec t R.empty v -> eval t v.

  Lemma decSamEam : forall (t : R.term) (c : R.context) (v : R.value), SAM.dec t c v -> dec t c v.
  Proof with eauto.
    induction 1 using SAM.dec_Ind with
    (P := fun t c v (H:SAM.dec t c v) => dec t c v)
    (P0:= fun c v v' (H:SAM.decctx c v v') => decctx c v v')
    (P1:= fun d v (H:SAM.iter d v) => match d with
                                        | R.d_val v' => decctx v R.empty v'
                                        | R.d_red r c => forall t c0,
                                                         R.contract r c = Some (t, c0) -> dec t c0 v
                                      end); simpl; intros.
    (* Case 1 *)
    inversion R_IT; subst; econstructor 1...
    (* Case 2 *)
    econstructor 2...
    (* Case 3 *)
    econstructor 3...
    (* Case 4 *)
    inversion IT_V; subst; constructor.
    (* Case 5 *)
    inversion_clear R_IT; econstructor 2...
    (* Case 6 *)
    econstructor 3...
    (* Case 7 *)
    econstructor 4...
    (* Case 8 *)
    constructor.
    (* Case 9 *)
    rewrite CONTR in H0; inversion H0; subst; auto.
  Qed.

  Lemma evalSamEam : forall (t : R.term) (v : R.value), SAM.eval t v -> eval t v.
  Proof.
    intros t v H; inversion_clear H; constructor; apply decSamEam; auto.
  Qed.
  Hint Resolve evalSamEam.

  Lemma decEamSam : forall (t : R.term) (c : R.context) (v : R.value), dec t c v -> SAM.dec t c v.
  Proof with eauto.
    induction 1 using dec_Ind with
    (P := fun t c v (H:dec t c v) => SAM.dec t c v)
    (P0:= fun v c v' (H:decctx v c v') => SAM.decctx v c v'); intros; simpl.
    econstructor 1; try econstructor...
    econstructor 2...
    econstructor 3...
    repeat constructor.
    econstructor 2; try econstructor 2...
    econstructor 3...
    econstructor 4...
  Qed.

  Lemma evalEamSam : forall (t : R.term) (v : R.value), eval t v -> SAM.eval t v.
  Proof.
    intros t v H; inversion_clear H; constructor; apply decEamSam; auto.
  Qed.
  Hint Resolve evalEamSam.

  Theorem evalEam : forall (t : R.term) (v : R.value), RS.RS.eval t v <-> eval t v.
  Proof with auto.
    intros t v; rewrite SAM.evalSam; split...
  Qed.

End EvalApplyMachineCS.

Module ProperEAMachineCS (R : RED_LANG_CS) (RS : RED_REF_SEM_CS R) <: PROPER_EA_MACHINE_CS R.

  Module EAM := EvalApplyMachineCS R RS.

  Definition dec_term := RS.dec_term.
  Definition dec_context := RS.dec_context.

  Definition dec_term_correct := RS.dec_term_correct.
  Definition dec_context_correct := RS.dec_context_correct.

  Inductive configuration : Set :=
  | c_init  : R.term -> configuration
  | c_eval  : R.term -> R.context -> configuration
  | c_apply : R.context -> R.value -> configuration
  | c_final : R.value -> configuration.

  Reserved Notation " a → b " (at level 40, no associativity).

  Inductive transition : configuration -> configuration -> Prop :=
  | t_init : forall (t : R.term), transition (c_init t) (c_eval t R.empty)
  | t_red  : forall (t t0 : R.term) (c c0 : R.context) (r : R.redex)
               (DT    : dec_term t = R.in_red r)
               (CONTR : R.contract r c = Some (t0, c0)),
               (c_eval t c) → (c_eval t0 c0)
  | t_val  : forall (t : R.term) (v : R.value) (c : R.context)
      	       (DT    : dec_term t = R.in_val v),
               (c_eval t c) → (c_apply c v)
  | t_term : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context)
               (DT    : dec_term t = R.in_term t0 ec),
               (c_eval t c) → (c_eval t0 (ec :: c))
  | t_cfin : forall (v : R.value),
               (c_apply R.empty v) → (c_final v)
  | t_cred : forall (v : R.value) (t : R.term) (ec : R.elem_context) (c c0 : R.context) (r : R.redex)
               (DC    : dec_context ec v = R.in_red r)
               (CONTR : R.contract r c = Some (t, c0)),
               (c_apply (ec :: c) v) → (c_eval t c0)
  | t_cval : forall (v v0 : R.value) (ec : R.elem_context) (c : R.context)
               (DC    : dec_context ec v = R.in_val v0),
               (c_apply (ec :: c) v) → (c_apply c v0)
  | t_cterm: forall (v : R.value) (t : R.term) (ec ec0 : R.elem_context) (c : R.context)
               (DC    : dec_context ec v = R.in_term t ec0),
               (c_apply (ec :: c) v) → (c_eval t (ec0 :: c))
  where " a → b " := (transition a b).

  Module AM : ABSTRACT_MACHINE
    with Definition term := R.term
    with Definition value := R.value
    with Definition configuration := configuration
    with Definition transition := transition
    with Definition c_init := c_init
    with Definition c_final := c_final.
    Definition term := R.term.
    Definition value := R.value.
    Definition configuration := configuration.
    Definition transition := transition.
    Definition c_init := c_init.
    Definition c_final := c_final.

    Inductive trans_close : configuration -> configuration -> Prop :=
    | one_step   : forall (c0 c1 : configuration), transition c0 c1 -> trans_close c0 c1
    | multi_step : forall (c0 c1 c2 : configuration), transition c0 c1 -> trans_close c1 c2 -> trans_close c0 c2.

    Inductive eval : term -> value -> Prop :=
    | e_intro : forall (t : term) (v : value), trans_close (c_init t) (c_final v) -> eval t v.

  End AM.

  Notation " a →+ b " := (AM.trans_close a b) (at level 40, no associativity).

  Lemma decEamTrans : forall (t:R.term) (c : R.context) (v:R.value), EAM.dec t c v -> (c_eval t c) →+ (c_final v).
  Proof with eauto.
    induction 1 using EAM.dec_Ind with
    (P := fun t c v (H:EAM.dec t c v) => (c_eval t c) →+ (c_final v))
    (P0:= fun v c v' (H:EAM.decctx v c v') =>  (c_apply c v) →+ (c_final v')); intros; simpl; auto;
    try (econstructor; econstructor; eauto; fail).
    econstructor 2; eauto; econstructor...
    econstructor 2; eauto; econstructor...
    econstructor 2; eauto; econstructor 4...
    econstructor 2; eauto; econstructor...
    econstructor 2; eauto; econstructor...
    econstructor 2; eauto; econstructor 8...
  Qed.
  Hint Resolve decEamTrans.

  Lemma evalEamMachine : forall (t : R.term) (v : R.value), EAM.eval t v -> AM.eval t v.
  Proof with eauto.
    intros t v H; inversion_clear H; constructor; econstructor 2 with (c_eval t R.empty); auto; constructor.
  Qed.
  Hint Resolve evalEamMachine.

  Lemma transDecEam : forall (t : R.term) (c : R.context) (v : R.value), (c_eval t c) →+ (c_final v) -> EAM.dec t c v.
  Proof with eauto.
    intros t c v X.
    refine (AM.trans_close_ind
    (fun c c0 =>match c, c0 with
      | c_eval t c, c_final v => EAM.dec t c v
      | c_apply c v, c_final v0 => EAM.decctx v c v0
      | _, _ => True
    end)
    _ _ (c_eval t c) (c_final v) X); intros; auto.
    (* Case 1 *)
    generalize H; clear H; case c0; case c1; simpl; intros; try inversion t2; subst; auto;
    inversion_clear H; constructor 1; auto.
    (* Case 2 *)
    generalize H H0 H1; clear H H0 H1; case c0; case c1; case c2; simpl; auto; intros; inversion H; subst.
    econstructor...
    econstructor 3...
    econstructor 2...
    econstructor...
    econstructor 4...
    econstructor 3...
    inversion H0; subst; inversion H2.
  Qed.
  Hint Resolve transDecEam.

  Lemma evalMachineEam : forall (t : R.term) (v : R.value), AM.eval t v -> EAM.eval t v.
  Proof with auto.
    intros t v H; inversion_clear H; constructor; inversion_clear H0; inversion H; subst...
  Qed.
  Hint Resolve evalMachineEam.

  Theorem eval_apply_correct : forall (t : R.term) (v : R.value), RS.RS.eval t v <-> AM.eval t v.
  Proof with auto.
    intros t v; rewrite EAM.evalEam; split...
  Qed.

End ProperEAMachineCS.

Module PushEnterMachineCS (R : RED_LANG_CS) (PRS : PE_REF_SEM R) <: PUSH_ENTER_MACHINE_CS R.

  Module EAM := EvalApplyMachineCS R PRS.Red_Sem.
  Module PR := Red_Prop R PRS.Red_Sem.

  Definition dec_term := PRS.Red_Sem.dec_term.
  Definition dec_context := PRS.Red_Sem.dec_context.
  Definition dec_context_not_val := PRS.dec_context_not_val.
  Definition dec_context_correct := PRS.Red_Sem.dec_context_correct.
  Definition dec_term_correct := PRS.Red_Sem.dec_term_correct.
  Definition dec_term_value := PRS.dec_term_value.

  Inductive dec : R.term -> R.context -> R.value -> Prop :=
  | dec_r    : forall (t t0 : R.term) (c c0 : R.context) (r : R.redex) (v : R.value)
                 (DT    : dec_term t = R.in_red r)
                 (CONTR : R.contract r c = Some (t0, c0))
                 (R_T   : dec t0 c0 v),
                 dec t c v
  | dec_val  : forall (t : R.term) (v : R.value)
                 (DT    : dec_term t = R.in_val v),
                 dec t R.empty v
  | dec_v_t  : forall (t t0 : R.term) (ec ec0 : R.elem_context) (c : R.context) (v v0 : R.value)
                 (DT    : dec_term t = R.in_val v)
                 (DC    : dec_context ec v = R.in_term t0 ec0)
                 (R_T   : dec t0 (ec0 :: c) v0),
                 dec t (ec :: c) v0
  | dec_red  : forall (t t0 : R.term) (ec : R.elem_context) (c c0 : R.context) (v v0 : R.value) (r : R.redex)
                 (DT    : dec_term t = R.in_val v)
                 (DC    : dec_context ec v = R.in_red r)
                 (CONTR : R.contract r c = Some (t0, c0))
                 (R_T   : dec t0 c0 v0),
                 dec t (ec :: c) v0
  | dec_rec  : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context) (v : R.value)
                 (DT    : dec_term t = R.in_term t0 ec)
                 (R_T   : dec t0 (ec :: c) v),
                 dec t c v.

  Scheme dec_Ind := Induction for dec Sort Prop.

  Inductive eval : R.term -> R.value -> Prop :=
  | e_intro : forall (t : R.term) (v : R.value), dec t R.empty v -> eval t v.

  Lemma decEamPem : forall (t : R.term) (c : R.context) (v : R.value), EAM.dec t c v -> dec t c v.
  Proof with eauto.
    induction 1 using EAM.dec_Ind with
    (P := fun t c v (H:EAM.dec t c v) => dec t c v)
    (P0:= fun v c v0 (H:EAM.decctx v c v0) =>
      match c with
      | nil => dec (R.value_to_term v) R.empty v0
      | (ec :: c) => forall d : R.interm_dec, dec_context ec v = d ->
        match d with
        | R.in_red r => forall t c0, R.contract r c = Some (t, c0) -> dec t c0 v0
        | R.in_term t ec0 => dec t (ec0 :: c) v0
        | R.in_val v => False
        end
      end); intros; simpl.
    (* Case 1 *)
    econstructor...
    (* Case 2 *)
    inversion R_C; subst.
    (* Case 2.1 *)
    constructor...
    (* Case 2.2 *)
    econstructor 4...
    apply (IHdec (R.in_red r))...
    (* Case 2.3 *)
    contradict (dec_context_not_val _ _ _ DC).
    (* Case 2.4 *)
    econstructor 3...
    apply (IHdec (R.in_term t0 ec0))...
    (* Case 3 *)
    econstructor 5...
    (* Case 4 *)
    constructor; apply dec_term_value...
    (* Case 5 *)
    change (EAM.dec_context ec v = d) in H0; rewrite DC in H0; inversion H0;
    subst; simpl; intros.
    rewrite CONTR in H0; inversion H0; subst; auto.
    (* Case 7 *)
    contradict (dec_context_not_val _ _ _ DC).
    (* Case 8 *)
    change (EAM.dec_context ec v = d) in H0; rewrite DC in H0; subst; simpl...
  Qed.

  Lemma evalEamPem : forall (t : R.term) (v : R.value), EAM.eval t v -> eval t v.
  Proof.
    intros t v H; inversion_clear H; constructor; apply decEamPem; auto.
  Qed.
  Hint Resolve evalEamPem.

  Lemma decPemEam : forall (t : R.term) (c : R.context) (v : R.value), dec t c v -> EAM.dec t c v.
  Proof with eauto.
    induction 1; intros; simpl; auto.
    econstructor 1...
    econstructor 2... econstructor...
    econstructor 2... econstructor 4...
    econstructor 2... econstructor 2...
    econstructor 3...
  Qed.

  Lemma evalPemEam : forall (t : R.term) (v : R.value), eval t v -> EAM.eval t v.
  Proof.
    intros t v H; inversion_clear H; constructor; apply decPemEam; auto.
  Qed.
  Hint Resolve evalPemEam.

  Theorem evalPem : forall (t : R.term) (v : R.value), PRS.Red_Sem.RS.eval t v <-> eval t v.
  Proof.
    intros t v; rewrite EAM.evalEam; split; auto.
  Qed.

End PushEnterMachineCS.

Module ProperPEMachineCS (R : RED_LANG_CS) (PRS : PE_REF_SEM R) <: PROPER_PE_MACHINE_CS R.

  Module PEM := PushEnterMachineCS R PRS.

  Definition dec_term := PRS.Red_Sem.dec_term.
  Definition dec_context := PRS.Red_Sem.dec_context.
  Definition dec_term_value := PEM.dec_term_value.
  Definition dec_context_not_val := PRS.dec_context_not_val.
  Definition dec_context_correct := PRS.Red_Sem.dec_context_correct.
  Definition dec_term_correct := PRS.Red_Sem.dec_term_correct.

  Inductive configuration : Set :=
  | c_init  : R.term -> configuration
  | c_eval  : R.term -> R.context -> configuration
  | c_final : R.value -> configuration.

  Reserved Notation " a → b " (at level 40, no associativity).

  Inductive transition : configuration -> configuration -> Prop :=
  | t_init : forall (t : R.term),
               c_init t → c_eval t R.empty
  | t_red  : forall (t t0 : R.term) (c c0 : R.context) (r : R.redex)
               (DT    : dec_term t = R.in_red r)
               (CONTR : R.contract r c = Some (t0, c0)),
               c_eval t c → c_eval t0 c0
  | t_cval : forall (t : R.term) (v : R.value)
               (DT    : dec_term t = R.in_val v),
               c_eval t R.empty → c_final v
  | t_cred : forall (t t0 : R.term) (v : R.value) (ec : R.elem_context) (c c0 : R.context) (r : R.redex)
               (DT    : dec_term t = R.in_val v)
               (DC    : dec_context ec v = R.in_red r)
               (CONTR : R.contract r c = Some (t0, c0)),
               c_eval t (ec :: c) → c_eval t0 c0
  | t_crec : forall (t t0 : R.term) (v : R.value) (ec ec0 : R.elem_context) (c : R.context)
               (DT    : dec_term t = R.in_val v)
               (DC    : dec_context ec v = R.in_term t0 ec0),
               c_eval t (ec :: c) → c_eval t0 (ec0 :: c)
  | t_rec  : forall (t t0 : R.term) (ec : R.elem_context) (c : R.context)
               (DT    : dec_term t = R.in_term t0 ec),
               c_eval t c → c_eval t0 (ec :: c)
  where " a →  b " := (transition a b).

  Module AM : ABSTRACT_MACHINE
    with Definition term := R.term
    with Definition value := R.value
    with Definition configuration := configuration
    with Definition transition := transition
    with Definition c_init := c_init
    with Definition c_final := c_final.
    Definition term := R.term.
    Definition value := R.value.
    Definition configuration := configuration.
    Definition transition := transition.
    Definition c_init := c_init.
    Definition c_final := c_final.

    Inductive trans_close : configuration -> configuration -> Prop :=
    | one_step   : forall (c0 c1 : configuration), transition c0 c1 -> trans_close c0 c1
    | multi_step : forall (c0 c1 c2 : configuration), transition c0 c1 -> trans_close c1 c2 -> trans_close c0 c2.

    Inductive eval : term -> value -> Prop :=
    | e_intro : forall (t : term) (v : value), trans_close (c_init t) (c_final v) -> eval t v.

  End AM.

  Notation " a →+ b " := (AM.trans_close a b) (at level 40, no associativity).

  Lemma decPemTrans : forall (t : R.term) (c : R.context) (v : R.value), PEM.dec t c v -> (c_eval t c) →+ (c_final v).
  Proof with eauto.
    induction 1; intros; simpl; try (constructor; econstructor; auto; fail); try (econstructor 2; eauto; econstructor; eauto; fail);
    econstructor 2; eauto.
    econstructor 5...
    econstructor 4...
    econstructor 6...
  Qed.
  Hint Resolve decPemTrans.

  Lemma evalPemMachine : forall (t : R.term) (v : R.value), PEM.eval t v -> AM.eval t v.
  Proof with eauto.
    intros t v H; inversion_clear H; constructor; econstructor 2; eauto; econstructor...
  Qed.
  Hint Resolve evalPemMachine.

  Lemma transDecPem : forall (t : R.term) (c : R.context) (v : R.value), (c_eval t c) →+ (c_final v) -> PEM.dec t c v.
  Proof with eauto.
    intros t c v X; refine (AM.trans_close_ind
    (fun c c0 => match c, c0 with
      | c_eval t c, c_final v => PEM.dec t c v
      | _, _ => True
    end) _ _ (c_eval t c) (c_final v) X); intros...
    generalize H; clear H; case c0; case c1; simpl; intros; try inversion t2; subst; auto; inversion_clear H; econstructor 2...
    generalize H H0 H1; clear H H0 H1; case c0; case c1; case c2; simpl; auto; intros; inversion H; subst.
    econstructor...
    econstructor 4...
    econstructor 3...
    econstructor 5...
    inversion H0; subst; inversion H2.
  Qed.
  Hint Resolve transDecPem.

  Lemma evalMachinePem : forall (t : R.term) (v : R.value), AM.eval t v -> PEM.eval t v.
  Proof.
    intros t v H; constructor; inversion_clear H; inversion H0; subst; inversion H; subst; auto.
  Qed.
  Hint Resolve evalMachinePem.

  Theorem push_enter_correct : forall (t : R.term) (v : R.value), PRS.Red_Sem.RS.eval t v <-> AM.eval t v.
  Proof.
    intros t v; rewrite (PEM.evalPem); split; auto.
  Qed.

End ProperPEMachineCS.

author: fsieczkowski

repo: Refocusing


text:
Require Import Bool List.

Require Import Arith.PeanoNat FSets.FMapWeakList.

Variable LocalPState : Type.

Module Import MapNat := FMapWeakList.Make Nat.

Section MachineDef.

Definition BusinessId := nat.
Definition BusinessMap := MapNat.t.

Definition GlobalPState := BusinessMap LocalPState.

Section Deal.

Definition Deal := (BusinessId * BusinessId * BusinessId) % type.
Parameter allows : BusinessId -> (BusinessId * BusinessId) -> option LocalPState.

Definition step_legal_deal (me : BusinessId) (deal : Deal) : Prop :=
  let '(a, b, c) := deal in
     (me = a /\ (allows me (b, c) <> None \/ allows me (c, b) <> None))
  \/ (me = b /\ (allows me (a, c) <> None \/ allows me (c, a) <> None))
  \/ (me = c /\ (allows me (a, b) <> None \/ allows me (b, a) <> None)).

Definition consistent_deal (deal : Deal) : Prop :=
  let '(a, b, c) := deal in
  step_legal_deal a deal /\ step_legal_deal b deal /\ step_legal_deal c deal.

End Deal.

Record Machine : Type := {
  history : list Deal;
}.

Inductive machine_step : Machine -> Machine -> Prop :=
  .

Variable startState : GlobalPState.
End MachineDef.

Section ArenaDef.

Definition AgentId := nat.
Definition AgentMap := MapNat.t.
(* business_of owner -> someother -> transitio *)

Definition Request : Type := LocalPState * LocalPState.

Parameter business_of : AgentId -> BusinessId.

Record Arena : Type := {
  billboard : AgentMap Request;
  machine : Machine;
}.
(* TODO: add state *)
Variable agents_actions : AgentMap (Arena -> Request).

Definition add_request (owner : AgentId) (request : Request) (a : Arena) : Arena :=
  Build_Arena (add owner request (billboard a)) (machine a).

Inductive arena_step : Arena -> Arena -> Prop :=
  | exec_request (owner : AgentId) (request : Request) : forall a1 a2,
                   billboard a2 = remove owner (billboard a1)
                 -> machine_step (machine a1) (machine a2)
                 -> arena_step a1 a2
  | agent_act (owner : AgentId) (request : Request) : forall (a1 : Arena),
                    Some request = find owner (map (fun s => s a1) agents_actions)
                 -> mem owner (billboard a1) = false
                 -> arena_step a1 (add_request owner request a1).

End ArenaDef.

author: elazarg

repo: blockchain

save_path: github-repos/coq/elazarg-blockchain


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal33.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Lemma conj10synthconj6 : forall  (lv0 : natural) (lv1 : natural), (@eq natural (mult (Succ lv0) (Succ lv1)) (plus (mult lv1 (Succ lv0)) (Succ lv0))).
Admitted.
QuickChick conj10synthconj6.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(* (c) Copyright Microsoft Corporation and Inria. You may distribute   *)
(* under the terms of either the CeCILL-B License or the CeCILL        *)
(* version 2 License, as specified in the README file.                 *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
Require Import seq fintype div bigops prime ssralg poly.
Require Import finset groups morphisms automorphism normal perm zmodp.

(***********************************************************************)
(*  Properties of cyclic groups                                        *)
(***********************************************************************)
(* Definitions:                                                        *)
(* Defined in groups.v:                                                *)
(*   <[x]>         == the cycle (cyclic group) generated by x          *)
(*   #[x]          == the order of x, i.e., the cardinal of <[x]>.     *)
(* Defined in phi.v:                                                   *)
(*   phi n         == Euler's totient function                         *)
(* In this file:                                                       *)
(*   cyclic G      <=> G is a cyclic group.                            *)
(*   generator G x <=> x is a generator of the (cyclic) group G.       *)
(*   Zpm x         == the isomorphism between the additive group of    *)
(*                    integers mod #[x], and the group <[x]>           *)
(*   cyclem x n    == the endomorphism y |-> y ^+ n of <[x]>           *)
(*   Zp_unitm x    == the isomorphism from the multiplicative group of *)
(*                    the units of the ring of integers mod #[x], with *)
(*                    the group Aut <[x]> of automorphisms of <[x]>.   *)
(*                    (Zp_unitm x map u to cyclem x u)                 *)
(* Basic results for these notions, plus the classical result that     *)
(* any finite group isomorphic to a subggroup of a field is cycle,     *)
(* and the corollary that Aut G is cyclic when G is of prime order.    *)
(***********************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Import GroupScope.

(***********************************************************************)
(*  Cyclic groups.                                                     *)
(***********************************************************************)

Section Cyclic.

Variable gT : finGroupType.
Implicit Types a x y : gT.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.

Definition cyclic A := existsb x, A == <[x]>.

Lemma cyclicP : forall A, reflect (exists x, A = <[x]>) (cyclic A).
Proof. move=> A; apply: (iffP existsP) => [] [x]; exists x; exact/eqP. Qed.

Lemma cycle_cyclic : forall x, cyclic <[x]>.
Proof. by move=> x; apply/cyclicP; exists x. Qed.

Lemma cyclic1 : cyclic [1 gT].
Proof. by rewrite -cycle1 cycle_cyclic. Qed.

(***********************************************************************)
(* Isomorphism with the additive group                                 *)
(***********************************************************************)

Section Zpm.

Variable a : gT.

Definition Zpm (i : 'I_#[a]) := a ^+ i.

Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}.
Proof. by move=> i j _ _; rewrite /Zpm /= expg_mod_order expgn_add. Qed.

Canonical Structure Zpm_morphism := Morphism ZpmM.

Lemma morphim_Zpm : Zpm @* Zp #[a] = <[a]>.
Proof.
apply/eqP; rewrite morphimEdom eq_sym eqEcard andbC.
rewrite -[#|<[a]>|]card_Zp leq_imset_card.
apply/subsetP=> x; case/cyclePmin=> i lt_i_a ->.
by apply/imsetP; exists (Ordinal lt_i_a); rewrite ?inE.
Qed.

Lemma Zpm_inj : injective Zpm.
Proof.
apply/injectiveP; apply/card_uniqP; rewrite size_map -cardE card_ord /=.
rewrite {5}/order -morphim_Zpm morphimEdom /=; apply: eq_card => x.
by apply/imageP/imsetP=> [] [i _ ->] /=; exists i; rewrite ?inE.
Qed.

Lemma injm_Zpm : 'injm Zpm.
Proof. apply/injmP; exact: (in2W Zpm_inj). Qed.

Lemma eq_expg_mod_order : forall m n,
  (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).
Proof.
move=> m n; symmetry; pose Za := inZp (order_gt0 a).
by rewrite -[_ == _](inj_eq Zpm_inj (Za m) (Za n)) /Zpm !expg_mod_order.
Qed.

Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm.
Proof. by apply/isomP; rewrite injm_Zpm morphim_Zpm. Qed.

Lemma Zp_isog : isog (Zp #[a]) <[a]>.
Proof. exact: isom_isog Zp_isom. Qed.

Lemma cycle_decomp : forall b,
  b \in <[a]> -> {m : nat | m < #[a] & a ^+ m = b}.
Proof.
move=> b; rewrite -morphim_Zpm; move/(invmK injm_Zpm).
by case: {+}(invm _ b) => m; exists m.
Qed.

End Zpm.

(***********************************************************************)
(*        Central and direct product of cycles                         *)
(***********************************************************************)

Lemma cents_cycle : forall a b, commute a b -> <[a]> \subset 'C(<[b]>).
Proof.
move=> a b cab; rewrite gen_subG centsC cent_set1 cycle_subG; exact/cent1P.
Qed.

Lemma cycle_abelian : forall a, abelian <[a]>.
Proof. move=> a; exact: cents_cycle. Qed.

Lemma cyclic_abelian : forall A, cyclic A -> abelian A.
Proof. move=> A; case/cyclicP=> a ->; exact: cycle_abelian. Qed.

Lemma cycleMsub : forall a b,
  commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>.
Proof.
move=> a b cab co_ab; apply/subsetP=> x; case/cycleP=> k ->{x}.
apply/cycleP; exists (chinese #[a] #[b] k 0); symmetry.
rewrite expMgn // -expg_mod_order chinese_modl // expg_mod_order.
by rewrite /chinese addn0 -mulnA mulnCA expgn_mul expg_order exp1gn mulg1.
Qed.

Lemma cycleM : forall a b,
  commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>.
Proof.
move=> a b cab co_ab; apply/eqP.
rewrite eqEsubset -(cent_mulgenEl (cents_cycle cab)).
rewrite mulgen_subG {3}cab !cycleMsub // 1?coprime_sym //.
by rewrite -genM_mulgen cycle_subG mem_gen // mem_imset2 ?cycle_id.
Qed.

(***********************************************************************)
(*        Order properties                                             *)
(***********************************************************************)

Lemma order_dvdn : forall a n, (#[a] %| n) = (a ^+ n == 1).
Proof. by move=> a n; rewrite (eq_expg_mod_order a n 0) mod0n. Qed.

Lemma order_inf : forall a n, a ^+ n.+1 == 1 -> #[a] <= n.+1.
Proof. move=> a n; rewrite -order_dvdn; exact: dvdn_leq. Qed.

Lemma order_eq1 : forall a, (#[a] == 1%N) = (a == 1).
Proof. by move=> a; rewrite -dvdn1 order_dvdn expg1. Qed.

Lemma cycle_eq1 : forall a, (<[a]> == 1) = (a == 1).
Proof. by move=> a; rewrite -order_eq1 trivg_card1. Qed.

Lemma order_dvdG : forall (G : {group gT}) a, a \in G -> #[a] %| #|G|.
Proof. by move=> G a Ga; apply: cardSg; rewrite cycle_subG. Qed.

Lemma orderXdvd : forall a n, #[a ^+ n] %| #[a].
Proof. move=> a n; apply: order_dvdG; exact: mem_cycle. Qed.

Lemma orderXgcd : forall a n, #[a ^+ n] = #[a] %/ gcdn #[a] n.
Proof.
move=> a n; apply/eqP; rewrite eqn_dvd; apply/andP; split.
  rewrite order_dvdn -expgn_mul -gcdn_divnC //.
  by rewrite expgn_mul expg_order exp1gn.
case: (posnP n) => [-> | n_gt0]; first by rewrite gcdn0 divnn order_gt0 dvd1n.
rewrite -(dvdn_pmul2r n_gt0) divn_mulAC ?dvdn_gcdl // dvdn_lcm.
by rewrite order_dvdn mulnC expgn_mul expg_order eqxx dvdn_mulr.
Qed.

Lemma orderXdiv : forall a n, n %| #[a] -> #[a ^+ n] = #[a] %/ n.
Proof.
by move=> a n; case/dvdnP=> q defq; rewrite orderXgcd {2}defq gcdnC gcdn_mull.
Qed.

Lemma orderM : forall a b : gT,
  commute a b -> coprime #[a] #[b] -> #[a * b] = (#[a] * #[b])%N.
Proof. by move=> a b Hcom Hcop; rewrite -coprime_cardMg -?cycleM. Qed.

(***********************************************************************)
(*        Generator                                                    *)
(***********************************************************************)

Definition generator (A : {set gT}) a := A == <[a]>.

Lemma generator_cycle : forall a, generator <[a]> a.
Proof. by move=> a; exact: eqxx. Qed.

Lemma cycle_generator : forall a x, generator <[a]> x -> x \in <[a]>.
Proof. move=> a x; move/(<[a]> =P _)->; exact: cycle_id. Qed.

Lemma generator_order : forall a b,
  generator <[a]> b -> #[a] = #[b].
Proof. by rewrite /order => a b; move/(<[a]> =P _)->. Qed.

End Cyclic.

(* Euler's theorem *)

Theorem Euler: forall a n, coprime a n -> a ^ phi n  = 1 %[mod n].
Proof.
move=> a n; case: (posnP n) => [-> //|n_gt0] co_a_n; pose n0 := PosNat n_gt0.
have Ua: coprime n0 (inZp n_gt0 a) by rewrite coprime_sym coprime_modl.
have: ZpUnit Ua ^+ phi n0 == 1.
  by rewrite -card_Zp_units -order_dvdn order_dvdG ?inE.
by rewrite -2!val_eqE /= (@Zp_units_expgn n0) /= modn_exp; move/eqP.
Qed.

Section CyclicSubGroup.

Variable gT : finGroupType.

(*  G. 1.3.1 (i) *)

Lemma cycle_sub_group : forall (a : gT) m, m %| #[a] ->
  [set H : {group gT} | (H \subset <[a]>) && (#|H| == m)]
     = [set <[a ^+ (#[a] %/ m)]>%G].
Proof.
move=> a m Hdiv.
have Hpos: 0 < m by apply (dvdn_gt0 (order_gt0 a) Hdiv).
have Hcardm: #|<[a ^+ (#[a] %/ m)]>| == m.
  rewrite [#|_|]orderXgcd -(divn_pmul2r Hpos) muln_gcdl divnK // gcdnC.
  by rewrite gcdn_mulr mulKn.
apply/eqP; rewrite eqEsubset sub1set inE /= cycleX Hcardm !andbT.
apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard (eqP Hcardm).
case/andP=> sXa; move/eqP=> oX; rewrite oX leqnn andbT.
apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x.
have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set.
rewrite def_x -expgn_mul -order_dvdn -[#[a]](LaGrange sXa) -oX mulnC.
rewrite dvdn_pmul2r // mulnK //; case/dvdnP=> i ->{def_x k}.
by rewrite mulnC expgn_mul groupX // cycle_id.
Qed.

Lemma cycle_subgroup_char : forall a (H : {group gT}),
  H \subset <[a]> -> H \char <[a]>.
Proof.
move=> a H sHa; apply: lone_subgroup_char => // J sJa isoJH.
have dvHa: #|H| %| #[a] by exact: cardSg.
have{dvHa} Huniq := esym (cycle_sub_group dvHa).
move/setP: Huniq => Huniq; move: (Huniq H) (Huniq J); rewrite !inE /=.
by rewrite sHa sJa (isog_card isoJH) eqxx; do 2!move/eqP <-.
Qed.

End CyclicSubGroup.

(***********************************************************************)
(*  Reflected boolean property and morphic image, injection, bijection *)
(***********************************************************************)

Section MorphicImage.

Variables aT rT : finGroupType.
Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
Hypothesis Dx : x \in D.

Lemma morphim_cycle : f @* <[x]> = <[f x]>.
Proof. by rewrite morphim_gen (sub1set, morphim_set1). Qed.

Lemma morph_order : #[f x] %| #[x].
Proof. by rewrite order_dvdn -morphX // expg_order morph1. Qed.

Lemma morph_generator : forall A, generator A x -> generator (f @* A) (f x).
Proof. by move=> A; move/(A =P _)->; rewrite /generator morphim_cycle. Qed.

End MorphicImage.

Section CyclicProps.

Variables gT : finGroupType.
Implicit Types G H K : {group gT}.
Implicit Types aT rT : finGroupType.

Lemma cyclicS : forall G H, H \subset G -> cyclic G -> cyclic H.
Proof.
move=> G H HsubG; case/cyclicP=> x gex; apply/cyclicP.
exists (x ^+ (#[x] %/ #|H|)); apply: congr_group; apply/set1P.
by rewrite -cycle_sub_group /order -gex ?cardSg // inE HsubG eqxx.
Qed.

Lemma cyclicJ:  forall G x, cyclic (G :^ x) = cyclic G.
Proof.
move=> G x; apply/cyclicP/cyclicP=> [[y] | [y ->]].
  by move/(canRL (conjsgK x)); rewrite -cycleJ; exists (y ^ x^-1).
by exists (y ^ x); rewrite cycleJ.
Qed.

Lemma morphim_cyclic :  forall rT G H (f : {morphism G >-> rT}),
  cyclic H -> cyclic (f @* H).
Proof.
move=> rT G H f cH; wlog sHG: H cH / H \subset G.
  by rewrite -morphimIdom; apply; rewrite (cyclicS _ cH, subsetIl) ?subsetIr.
case/cyclicP: cH sHG => x ->; rewrite gen_subG sub1set => Gx.
by apply/cyclicP; exists (f x); rewrite morphim_cycle.
Qed.

Lemma quotient_cycle : forall x H, x \in 'N(H) -> <[x]> / H = <[coset H x]>.
Proof. move=> x H; exact: morphim_cycle. Qed.

Lemma quotient_cyclic : forall G H, cyclic G -> cyclic (G / H).
Proof. move=> G H; exact: morphim_cyclic. Qed.

Lemma quotient_generator : forall x G H,
  x \in 'N(H) -> generator G x -> generator (G / H) (coset H x).
Proof. by move=> x G H Nx; apply: morph_generator. Qed.

Lemma prime_cyclic : forall G, prime #|G| -> cyclic G.
Proof.
move=> G pG; case: (pickP (mem G^#)) => [x Hx| Hx]; last first.
  by move: pG; rewrite (cardsD1 1 G) group1 (eq_card0 Hx).
move: (Hx); rewrite /= in_setD1; case/andP => xD1; rewrite -cycle_subG=> xIG.
case/primeP: pG => _; move/(_ _ (cardSg xIG)); case/orP;  move/eqP.
  by rewrite (cardsD1 1) (cardsD1 x) group1 in_setD1 xD1 cycle_id.
move=> CxG; apply/cyclicP; exists x.
by apply/eqP; rewrite eq_sym eqEcard // CxG leqnn andbT.
Qed.

Lemma cyclic_small : forall G, #|G| <= 3 -> cyclic G.
Proof.
move=> G; rewrite 4!(ltnS, leq_eqVlt) -trivg_card_le1 orbA orbC.
case/predU1P=> [->|oG]; first exact: cyclic1.
by apply: prime_cyclic; case/pred2P: oG => ->.
Qed.

End CyclicProps.

Section IsoCyclic.

Variables gT rT : finGroupType.
Implicit Types G H : {group gT}.
Implicit Types M : {group rT}.

Lemma injm_cyclic :  forall G H (f : {morphism G >-> rT}),
  'injm f -> H \subset G -> cyclic (f @* H) = cyclic H.
Proof.
move=> G H f injf sHG; apply/idP/idP; last exact: morphim_cyclic.
rewrite -{2}(morphim_invm injf sHG); exact: morphim_cyclic.
Qed.

Lemma isog_cyclic :forall G M, G \isog M -> cyclic G = cyclic M.
Proof. by move=> G M; case/isogP=> f injf <-; rewrite injm_cyclic. Qed.

Lemma isog_cyclic_card : forall G M,
  cyclic G -> isog G M = cyclic M && (#|M| == #|G|).
Proof.
move=> G H cycG; apply/idP/idP=> [isoGM | ].
  by rewrite (isog_card isoGM) -(isog_cyclic isoGM) cycG /=.
case/cyclicP: cycG => x ->{G}; case/andP; case/cyclicP=> y ->{M} oy.
apply: isog_trans (isog_symr _) (Zp_isog y).
by rewrite ((order_pos_nat y =P order_pos_nat x) _) // Zp_isog.
Qed.

Lemma injm_generator : forall G H (f : {morphism G >-> rT}) x,
    'injm f -> x \in G -> H \subset G ->
  generator (f @* H) (f x) = generator H x.
Proof.
move=> G H f x injf Gx sHG; apply/idP/idP; last exact: morph_generator.
rewrite -{2}(morphim_invm injf sHG) -{2}(invmE injf Gx).
apply: morph_generator; exact: mem_morphim.
Qed.

End IsoCyclic.

(***********************************************************************)
(*       Automorphisms of cyclic groups                                *)
(***********************************************************************)

Section CyclicAutomorphism.

Variable gT : finGroupType.

Section CycleAutomorphism.

Variable a : gT.

Section CycleMorphism.

Variable n : nat.

Definition cyclem of gT := fun x : gT => x ^+ n.

Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x * y}}.
Proof.
move=> x y ax ay; apply: expMgn; exact: (centsP (cycle_abelian a)).
Qed.

Canonical Structure cyclem_morphism := Morphism cyclemM.

End CycleMorphism.

Section ZpUnitMorphism.

Variable u : Zp_unit #[a].

Lemma injm_cyclem : 'injm (cyclem u a).
Proof.
apply/subsetP=> x; case/setIdP=> ax; rewrite !inE -order_dvdn.
rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-.
by rewrite dvdn_gcd order_dvdG.
Qed.

Lemma cyclem_dom : cyclem u a @* <[a]> = <[a]>.
Proof.
apply/morphim_fixP=> //; first exact: injm_cyclem.
by rewrite morphim_cycle ?cycle_id ?cycleX.
Qed.

Definition Zp_unitm := aut injm_cyclem cyclem_dom.

End ZpUnitMorphism.

Lemma Zp_unitmM : {in Zp_units #[a] &, {morph Zp_unitm : u v / u * v}}.
Proof.
move=> u v _ _; apply: (eq_Aut (Aut_aut _ _)) => [|x a_x].
  by rewrite groupM ?Aut_aut.
rewrite permM !autE ?groupX //= /cyclem -expgn_mul.
by rewrite -expg_mod_order modn_dvdm ?expg_mod_order // order_dvdG.
Qed.

Canonical Structure Zp_unit_morphism := Morphism Zp_unitmM.

Lemma injm_Zp_unitm : 'injm Zp_unitm.
Proof.
apply/subsetP=> u; case/morphpreP=> _; move/set1P=> /= um1.
have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1.
by rewrite !autE ?cycle_id // eq_expg_mod_order !modZp inE.
Qed.

Lemma generator_coprime : forall m, generator <[a]> (a ^+ m) = coprime #[a] m.
Proof.
move=> m; rewrite /generator eq_sym eqEcard cycleX -/#[a] [#|_|]orderXgcd /=.
apply/idP/idP=> [le_a_am|co_am]; last by rewrite (eqnP co_am) divn1.
have am_gt0: 0 < gcdn #[a] m by rewrite gcdn_gt0 order_gt0.
by rewrite /coprime eqn_leq am_gt0 andbT -(@leq_pmul2l #[a]) ?muln1 -?leq_divr.
Qed.

Lemma morphim_Zp_unitm : Zp_unitm @* Zp_units #[a] = Aut <[a]>.
Proof.
rewrite morphimEdom; apply/setP=> f; apply/imsetP/idP=> [[u _ ->] | Af].
  exact: Aut_aut.
pose n := invm (injm_Zpm a) (f a).
have a_fa: <[a]> = <[f a]>.
  by rewrite -(autmE Af) -morphim_cycle ?autm_dom ?cycle_id.
have def_n: a ^+ n = f a.
  by rewrite -/(Zpm n) invmK // morphim_Zpm a_fa cycle_id.
have co_a_n : coprime #[a] n by rewrite -generator_coprime def_n; exact/eqP.
exists (ZpUnit co_a_n); rewrite ?inE //.
apply: eq_Aut (Af) (Aut_aut _ _) _ => x ax.
rewrite autE //= /cyclem; case/cycleP: ax => k ->{x}.
by rewrite -(autmE Af) morphX ?cycle_id //= autmE -def_n -!expgn_mul mulnC.
Qed.

Lemma Zp_unit_isom : isom (Zp_units #[a]) (Aut <[a]>) Zp_unitm.
Proof. by apply/isomP; rewrite ?injm_Zp_unitm ?morphim_Zp_unitm. Qed.

Lemma Zp_unit_isog : isog (Zp_units #[a]) (Aut <[a]>).
Proof. exact: isom_isog Zp_unit_isom. Qed.

Lemma card_Aut_cycle : #|Aut <[a]>| = phi #[a].
Proof. by rewrite -(isog_card Zp_unit_isog) card_Zp_units. Qed.

Lemma phi_gen : phi #[a] = #|[set x | generator <[a]> x]|.
Proof.
rewrite -(card_injm (injm_invm (injm_Zpm a))) /= ?morphim_Zpm.
  rewrite -card_Zp_units cardsE card_sub morphim_invmE.
  by apply: eq_card => d; rewrite !inE /= -generator_coprime.
apply/subsetP=> x; rewrite inE; exact: cycle_generator.
Qed.

Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
Proof. by rewrite -morphim_Zp_unitm morphim_abelian ?Zp_units_abelian. Qed.

End CycleAutomorphism.

Variable G : {group gT}.

Lemma Aut_cyclic_abelian : cyclic G -> abelian (Aut G).
Proof. case/cyclicP=> x ->; exact: Aut_cycle_abelian. Qed.

Lemma card_Aut_cyclic : cyclic G -> #|Aut G| = phi #|G|.
Proof. case/cyclicP=> x ->; exact: card_Aut_cycle. Qed.

Lemma sum_ncycle_phi :
  \sum_(d < #|G|.+1) #|[set <[x]> | x <- G, #[x] == d]| * phi d = #|G|.
Proof.
pose h (x : gT) : 'I_#|G|.+1 := inord #[x].
symmetry; rewrite -{1}sum1_card (partition_big h xpredT) //=.
apply: eq_bigr => d _; set Gd := finset _.
rewrite -sum_nat_const sum1dep_card -sum1_card (_ : finset _ = Gd); last first.
  apply/setP=> x; rewrite !inE; case Gx: (x \in G) => //.
  by rewrite /eq_op /= inordK // ltnS subset_leq_card ?cycle_subG.
rewrite (partition_big_imset cycle) {}/Gd; apply: eq_bigr => C /=.
case/imsetP=> x; case/setIdP=> Gx; move/eqP=> <- -> {C d}.
rewrite sum1dep_card phi_gen; apply: eq_card => y; rewrite !inE /generator.
move: Gx; rewrite andbC eq_sym -!cycle_subG /order.
by case: (<[x]> == <[y]>) / (<[x]> =P <[y]>) => // -> ->; exact: eqxx.
Qed.

End CyclicAutomorphism.

Lemma sum_phi_dvd : forall n, \sum_(d < n.+1 | d %| n) phi d = n.
Proof.
move=> n; rewrite big_mkcond /=.
case: (posnP n) => [-> | n_gt0]; first by rewrite big_ord_recl big_ord0.
pose n0 := PosNat n_gt0; pose x1 : 'I_n0 := Zp_gen.
have ox1 : #[x1] = n by rewrite /order -Zp_cycle card_Zp.
rewrite -{8}ox1 -[#[_]]sum_ncycle_phi [#|_|]ox1; apply: eq_bigr => d _.
rewrite -{2}ox1; case: ifP => [|ndv_dG]; last first.
  rewrite eq_card0 // => C; apply/imsetP=> [[x]]; case/setIdP=> Gx oxd _{C}.
  by rewrite -(eqP oxd) order_dvdG in ndv_dG.
move/cycle_sub_group; set Gd := [set _] => def_Gd.
rewrite (_ : _ @: _ = @gval _ @: Gd); first by rewrite imset_set1 cards1 mul1n.
apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]].
  case/imsetP=> x; case/setIdP=> _ oxd ->; exists <[x]>%G => //.
  by rewrite -def_Gd inE -Zp_cycle subsetT.
have:= GdC; rewrite -def_Gd; case/setIdP=> _; move/eqP=> <-.
by rewrite (set1P GdC) /= mem_imset // inE eqxx (mem_cycle x1).
Qed.

Section FieldMulCyclic.

(***********************************************************************)
(* A classic application to finite multiplicative subgroups of fields. *)
(***********************************************************************)

Import GRing.Theory.

Variables (gT : finGroupType) (G : {group gT}).

Lemma order_inj_cyclic :
  {in G &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G.
Proof.
move=> ucG; apply: negbNE (contra _ (negbT (ltnn #|G|))) => ncG.
rewrite -{2}[#|G|]sum_phi_dvd big_mkcond (bigD1 ord_max) ?dvdnn //=.
rewrite -{1}[#|G|]sum_ncycle_phi (bigD1 ord_max) //= -addSn leq_add //.
  rewrite eq_card0 ?phi_gt0 ?cardG_gt0 // => C.
  apply/imsetP=> [[x]]; case/setIdP=> Gx; move/eqP=> oxG; case/cyclicP: ncG.
  by exists x; apply/eqP; rewrite eq_sym eqEcard cycle_subG Gx -oxG /=.
apply: (big_rel (fun a b => a <= b)) => // [*|d _]; first exact: leq_add.
set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0.
rewrite {}/Gd; case/imsetP=> x; case/setIdP=> Gx; move/eqP=> <- _ {C d}.
rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C.
apply/idP/eqP=> [|-> {C}]; last by rewrite mem_imset // inE Gx eqxx.
by case/imsetP=> y; case/setIdP=> Gy; move/eqP; move/ucG->.
Qed.

Lemma div_ring_mul_group_cyclic : forall (R : unitRingType) (f : gT -> R),
    f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
    {in G^#, forall x, GRing.unit (f x - 1)%R} ->
  abelian G -> cyclic G.
Proof.
move=> R f f1 fM f1P abelG.
have fX: forall n, {in G, {morph f : u / u ^+ n >-> (u ^+ n)%R}}.
  by case=> // n x Gx; elim: n => //= n IHn; rewrite expgS fM ?groupX ?IHn.
have fU: forall x, x \in G -> GRing.unit (f x).
  move=> x Gx; apply/unitrP.
  by exists (f x^-1); rewrite -!fM ?groupV ?gsimp.
apply: order_inj_cyclic => x y Gx Gy; set n := #[x] => yn.
apply/eqP; rewrite eq_sym eqEcard -[#|_|]/n yn leqnn andbT cycle_subG /=.
suff{y Gy yn} ->: <[x]> = G :&: [set z | #[z] %| n] by rewrite !inE Gy yn /=.
apply/eqP; rewrite eqEcard subsetI cycle_subG {}Gx /= cardE; set rs := enum _.
apply/andP; split; first by apply/subsetP=> y xy; rewrite inE order_dvdG.
pose P : {poly R} := ('X^n - 1)%R; have n_gt0: n > 0 by exact: order_gt0.
have szP: size P = n.+1 by rewrite size_addl size_polyXn ?size_opp ?size_poly1.
rewrite -ltnS -szP -(size_map f) max_ring_poly_roots -?size_poly_eq0 ?{}szP //.
  apply/allP=> fy; case/mapP=> y; rewrite mem_enum !inE order_dvdn.
  case/andP=> Gy; move/eqP=> yn1 ->{fy}; apply/eqP.
  by rewrite !(horner_lin, hornerXn) -fX // yn1 f1 subrr.
have: uniq rs by exact: enum_uniq.
have: all (mem G) rs by apply/allP=> y; rewrite mem_enum; case/setIP.
elim: rs => //= y rs IHrs; case/andP=> Gy Grs; case/andP=> y_rs; rewrite andbC.
move/IHrs=> -> {IHrs}//; apply/allP=> fz; case/mapP=> z rs_z ->{fz}.
have{Grs} Gz := allP Grs z rs_z; rewrite /diff_root -!fM // (centsP abelG) //.
rewrite eqxx -[f y]mul1r -(mulgKV y z) fM ?groupM ?groupV //=.
rewrite -mulNr -mulr_addl unitr_mull ?fU ?f1P // !inE.
by rewrite groupM ?groupV // andbT -eq_mulgV1; apply: contra y_rs; move/eqP <-.
Qed.

Lemma field_mul_group_cyclic : forall (F : fieldType) (f : gT -> F),
    {in G &, {morph f : u v / u * v >-> (u * v)%R}} ->
    {in G, forall x, f x = 1%R <-> x = 1} ->
  cyclic G.
Proof.
move=> F f fM f1P; have f1 : f 1 = 1%R by exact/f1P.
apply: (div_ring_mul_group_cyclic f1 fM) => [x|].
  case/setD1P=> x1 Gx; rewrite unitfE; apply: contra x1.
  by rewrite subr_eq0; move/eqP; move/f1P->.
apply/centsP=> x Gx y Gy; apply/commgP; apply/eqP.
apply/f1P; rewrite ?fM ?groupM ?groupV //.
by rewrite mulrCA -!fM ?groupM ?groupV // mulKg mulVg.
Qed.

End FieldMulCyclic.

(***********************************************************************)
(*  Cycles of prime order                                              *)
(***********************************************************************)

Section AutPrime.

Variable gT : finGroupType.

Lemma Aut_prime_cycle_cyclic : forall a : gT, prime #[a] -> cyclic (Aut <[a]>).
Proof.
move=> a pr_a; pose ff f := invm (injm_Zp_unitm a) f : Fp_field pr_a.
apply: (@field_mul_group_cyclic _ _ _ ff) => [f g Af Ag | f Af].
  by apply: val_inj; rewrite /ff morphM ?morphim_Zp_unitm.
split=> [/= ff1 |->]; last by apply: val_inj; rewrite /ff morph1.
apply: (injm1 (injm_invm (injm_Zp_unitm a))).
  by rewrite /= morphim_Zp_unitm.
by do 2!apply: val_inj; move/(congr1 val): ff1.
Qed.

Lemma Aut_prime_cyclic : forall G : {group gT}, prime #|G| -> cyclic (Aut G).
Proof.
move=> G pr_G; case/cyclicP: (prime_cyclic pr_G) (pr_G) => x ->.
exact: Aut_prime_cycle_cyclic.
Qed.

End AutPrime.

author: Wassasin

repo: ssreflect

save_path: github-repos/coq/Wassasin-ssreflect


text:
Require Import ExtLib.Data.PList.

Require Import MirrorCore.Lambda.Expr.
Require Import MirrorCore.Simple.
Require Import MirrorCore.Lib.ListView.
Require Import MirrorCore.Lib.ListOpView.
Require Import MirrorCore.Lib.NatView.
Require Import MirrorCore.Views.ViewSumN.
Require Import MirrorCore.syms.SymOneOf.
Require Import MirrorCore.syms.SymEnv.
Require Import MirrorCore.Subst.FMapSubst.
Require Import MirrorCore.Reify.Reify.
Require Import MirrorCore.Reify.ReifyClass.
Require Import MirrorCore.Reify.ReifyView.

Require Import McExamples.PolyApply.MSimpleType.

Import OneOfType.

Definition func_map :
  OneOfType.pmap :=
  list_to_pmap
    (pcons (listOp_func typ)
           (pcons (list_func typ)
                  (pcons SymEnv.func
                         (pcons natFunc
                                pnil)))).

Definition func := OneOf func_map.

Global Instance TableView_func : PartialView func SymEnv.func :=
  PartialViewPMap 3 func_map eq_refl.
Global Instance NatView_func : PartialView func natFunc :=
  PartialViewPMap 4 func_map eq_refl.
Global Instance ListView_func : PartialView func (list_func typ) :=
  PartialViewPMap 2 func_map eq_refl.
Global Instance ListOpView_func : PartialView func (listOp_func typ) :=
  PartialViewPMap 1 func_map eq_refl.

Class Environment := { simple_env :> @SymEnv.functions typ _}.

Existing Instance RelDec_from_RType.

Section SimpleFunc.

  Context {fs : Environment}.

  Global Instance RSym_func : RSym func.
  Proof.
    apply RSymOneOf.
    repeat first [eapply RSym_All_Branch_None |
                  eapply RSym_All_Branch_Some |
                  eapply RSym_All_Empty].

    apply RSym_ListOpFunc.
    apply RSym_ListFunc.
    apply RSym_NatFunc.
    apply RSym_func; apply fs.
  Defined.

  Global Instance RSymOk_func : RSymOk RSym_func.
  apply RSymOk_OneOf.

  repeat first [eapply RSymOk_All_Branch_None |
                eapply RSymOk_All_Branch_Some; [apply _ | |] |
                eapply RSymOk_All_Empty].
  Defined.

  Global Instance Expr_expr : ExprI.Expr _ (expr typ func) := @Expr_expr typ func _ _ _.
  Global Instance Expr_ok : @ExprI.ExprOk typ RType_typ (expr typ func) Expr_expr := @ExprOk_expr _ _ _ _ _ _ _ _.

  Require Import MirrorCore.VariablesI.
  Require Import MirrorCore.Lambda.ExprVariables.

  Global Instance ExprVar_expr : ExprVar (expr typ func) := _.
  Global Instance ExprVarOk_expr : ExprVarOk ExprVar_expr := _.

  Global Instance ExprUVar_expr : ExprUVar (expr typ func) := _.
  Global Instance ExprUVarOk_expr : ExprUVarOk ExprUVar_expr := _.

  Definition subst : Type :=
    FMapSubst.SUBST.raw (expr typ func).
  Global Instance SS : SubstI.Subst subst (expr typ func) :=
    @FMapSubst.SUBST.Subst_subst _.
  Global Instance SU : SubstI.SubstUpdate subst (expr typ func) :=
    @FMapSubst.SUBST.SubstUpdate_subst _ _ _ _.
Check SubstI.SubstOk.
  Global Instance SO : @SubstI.SubstOk _ _ _ _ _ SS :=
    @FMapSubst.SUBST.SubstOk_subst typ RType_typ (expr typ func) _.
  Global Instance SUO : @SubstI.SubstUpdateOk _ _ _ _ _ _ SU SO :=  @FMapSubst.SUBST.SubstUpdateOk_subst typ RType_typ (expr typ func) _ _.

End SimpleFunc.

Section ReifyFunc.

  Global Instance Reify_func : Reify (expr typ func) :=
    Reify_func typ func (reify_nat typ func :: reify_list typ func :: reify_listOp typ func :: nil).

End ReifyFunc.

Definition rt := reify_scheme typ.
Definition re := reify_scheme (expr typ func).

Reify Declare Syntax patterns_simple_typ := rt.
Reify Declare Syntax patterns_simple_expr := re.

Ltac reify trm :=
  let t := fresh "t" in
  let k e := pose e as t
  in
  reify_expr patterns_simple_expr k [[ True ]] [[ trm ]]; cbv beta iota in t.

Goal True.
  reify (In 5 (5::4::3::nil)).

  apply I.
Qed.
(*
SearchAbout In.
Require Import MirrorCore.Lemma.
Require Import MirrorCore.Polymorphic.

Instance Reify_lemma : Reify (lemma typ (expr typ func) (expr typ func)).
Check @Reify_rlemma typ (expr typ func).
Admitted.

Definition lem_in_eq : polymorphic typ 1 (Lemma.lemma typ (expr typ func) (expr typ func)) :=
Eval unfold Lemma.add_var, Lemma.add_prem, Lemma.vars, Lemma.concl, Lemma.premises in
  <:: @in_eq ::>.

SearchAbout Reify Lemma.lemma.

unfold Lemma.mkLemma.
 :=
  Eval unfold Lemma.add_var, Lemma.add_prem , Lemma.vars , Lemma.concl , Lemma.premises in
*)

author: gmalecha

repo: mirror-core

save_path: github-repos/coq/gmalecha-mirror-core


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall A B C D Aprime Bprime Cprime Dprime X Y E Z : Universe, ((wd_ X A /\ (wd_ X Aprime /\ (wd_ X C /\ (wd_ X Cprime /\ (wd_ Y B /\ (wd_ Y Bprime /\ (wd_ Y D /\ (wd_ Y Dprime /\ (wd_ A C /\ (wd_ B D /\ (wd_ A Aprime /\ (wd_ E Z /\ (wd_ X Y /\ (wd_ X B /\ (wd_ A Y /\ (wd_ A B /\ (wd_ B C /\ (wd_ Bprime Cprime /\ (wd_ A D /\ (wd_ Aprime Dprime /\ (wd_ Aprime Bprime /\ (wd_ A E /\ (col_ X A C /\ (col_ X A Aprime /\ (col_ X A Cprime /\ (col_ Y B D /\ (col_ Y B Bprime /\ (col_ Y B Dprime /\ (col_ E A B /\ (col_ E C D /\ (col_ X E Z /\ col_ A E Z))))))))))))))))))))))))))))))) -> col_ B E Z)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
(*–––––––––––––––––––––––––––––––––––+
 |
 |  Euclid's Axioms for Geometry
 |
 +–––––––––––––––––––––––––––––––––––*)

(* Basic Types *)
Axiom Point : Set.
Axiom origin : Point.

(*
 * Axiom 1: The Segment
 *)
Inductive Segment : Set :=
| segment_from_points : Point -> Point -> Segment.

(* The Distance measure*)
Axiom Distance : Set.
Axiom zero_distance : Distance.
Axiom distance_between : Segment -> Distance.

(*
 * Axiom 2: The Line
 *)
Inductive Line : Set :=
| line_from_segment : Segment -> Line.

(*
 * Axiom 3: The Circle
 *)
Inductive Circle : Set :=
| circle_from_segment : Segment -> Circle.

(*
 * Axiom 4: The Right Angle
 *)
Axiom Angle : Set.
Axiom right : Angle.

(* The Angle measure *)
Axiom angle_between : Line -> Line -> Angle.

Axiom lines_angles_equality:
  forall l l' l'' : Line,
  angle_between l l'  = angle_between l l''
  -> l' = l''.

(* example of lines angles equality *)
Proposition lines_right_angles_equality:
  forall l l' l'',
  angle_between l l'  = right
  -> angle_between l l'' = right
  -> l' = l''.
Proof.
  intros.
  cut (angle_between l l' = angle_between l l''). intro.
  apply (lines_angles_equality l l' l'' H1).
  pose (H1 := eq_sym H0).
  apply (eq_trans H H1).
Qed.

Inductive right_angled : Line -> Line -> Prop :=
  right_lines : forall l l', angle_between l l' = right -> right_angled l l'.

(* Axiom 5 *)
Axiom nonperpendicular_lines_intersect:
  forall l l',
  ~ right_angled l l'

repo: Coq-Work


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.solinas32_2e452m3_18limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition mul :
  { mul : feBW_loose -> feBW_loose -> feBW_tight
  | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_mul ().
  Show Ltac Profile.
Time Defined.

Print Assumptions mul.