Module group_ref

Time-stamp: "02/08/19 09:57:46 maggesi"

Require Export Field_Compl.
Require Arith.
Require EqNat.
Require Peano_dec.
Require Compare_dec.
Require BoolEq.
Require Export group.

Implicit Arguments On.

Lemma beq_nat_not_ref : (n,m:nat) ~(n=m) -> (beq_nat n m)=false.
Proof.
  Intros; Symmetry; Apply not_eq_false_beq with A:=nat; Auto.
  Intros; Apply beq_nat_eq; Assumption.
Qed.
Fixpoint blt_nat [n:nat] : nat -> bool :=
  [m:nat]Cases m n of
                0 _ => false
             | (S _) O => true
             | (S m1) (S n1) => (blt_nat n1 m1)
          end.

Lemma blt_imp_lt : (n,m:nat) (blt_nat n m)=true -> (lt n m).
Proof.
  Double Induction 1 2; Simpl; Intros; Auto with arith;
  Absurd false=true; Discriminate.
Qed.

Lemma lt_imp_blt : (n,m:nat) (lt n m) -> (blt_nat n m)=true.
Proof.
  Double Induction 1 2; Intros; Auto with arith; Simpl.
  Absurd (lt n (0)); Auto with arith.
  Absurd (lt (S n0) (0)); Auto with arith.
  Simpl; Auto with arith.
Qed.

Lemma lt_imp_not_blt : (n,m:nat) (lt n m) -> (blt_nat m n)=false.
Proof.
  Double Induction 1 2; Intros; Auto with arith; Simpl.
  Absurd (lt (S n0) (0)); Auto with arith.
  Auto with arith.
Qed.

Lemma lt_not_refl : (n:nat) (blt_nat n n)=false.
Proof.
  NewInduction n; Auto.
Qed.

Group Reflection

Section Group_Reflection.
  Variable A : Type.
  Variable op : A->A->A.
  Variable id : A.
  Variable iv : A->A.

  Hypothesis AT : (CGroup_Theory op id iv).

  Inductive expr : Type :=
  | Eatom : nat -> expr
  | Eid : expr
  | Eop : expr -> expr -> expr
  | Eiv : expr -> expr.

Note: The unbound variables are mapped to id. Normally this case sould never occur in practice.

  Local assoc2 [lvar:(listT (Sprod A nat));n:nat] : A :=
    (assoc_2nd A nat eq_nat_dec lvar n id).

  Fixpoint expr_interp [lvar:(listT (Sprod A nat));e:expr] : A :=
    Cases e of
    | Eid => id
    | (Eop e1 e2) => (op (expr_interp lvar e1) (expr_interp lvar e2))
    | (Eiv e) => (iv (expr_interp lvar e))
    | (Eatom n) => (assoc2 lvar n)
    end.

Implement groups as lists.

  Inductive lgrp : Set :=
  | lgrp_nil : lgrp
  | lgrp_cons : nat -> lgrp -> lgrp
  | lgrp_snoc : nat -> lgrp -> lgrp.

Interpretation function lgrp -> A.

  Fixpoint lgrp_interp [lvar:(listT (Sprod A nat));l:lgrp] : A :=
    Cases l of
    | lgrp_nil => id
    | (lgrp_cons i lgrp_nil) => (assoc2 lvar i)
    | (lgrp_cons i l1) => (op (assoc2 lvar i) (lgrp_interp lvar l1))
    | (lgrp_snoc i lgrp_nil) => (iv (assoc2 lvar i))
    | (lgrp_snoc i l1) => (op (iv (assoc2 lvar i)) (lgrp_interp lvar l1))
    end.

An other interpetation function in the proofs.

  Fixpoint lgrp_interp1 [lvar:(listT (Sprod A nat));l:lgrp] : A :=
    Cases l of
    | lgrp_nil => id
    | (lgrp_cons i l1) => (op (assoc2 lvar i) (lgrp_interp1 lvar l1))
    | (lgrp_snoc i l1) => (op (iv (assoc2 lvar i)) (lgrp_interp1 lvar l1))
    end.

The first and the second interpretation function are interchangables.

  Remark lgrp_interp_ok :
    (lvar:(listT (Sprod A nat));l:lgrp)
    (lgrp_interp lvar l) == (lgrp_interp1 lvar l).
  Proof.
    NewInduction l; Simpl; Try Reflexivity;
    Rewrite IHl; NewDestruct l; Simpl; Auto.
    Rewrite (group_dx_id AT); Reflexivity.
    Rewrite (group_dx_id AT); Reflexivity.
  Qed.

  Fixpoint lgrp_inv [l:lgrp] : lgrp :=
    Cases l of
    | lgrp_nil => lgrp_nil
    | (lgrp_cons i l1) => (lgrp_snoc i (lgrp_inv l1))
    | (lgrp_snoc i l1) => (lgrp_cons i (lgrp_inv l1))
    end.

  Remark lgrp_inv_ok1 :
    (lvar:(listT (Sprod A nat));l:lgrp)
    (lgrp_interp1 lvar (lgrp_inv l)) == (iv (lgrp_interp1 lvar l)).
  Proof.
    NewInduction l; Simpl.

    Symmetry; Apply (group_iv_id AT).

    Rewrite IHl; Simpl.
    Rewrite (group_iv_op AT).
    Apply (cgroup_comm AT).

    Rewrite IHl; Simpl.
    Rewrite (group_iv_op AT).
    Rewrite (group_iv_iv AT).
    Apply (cgroup_comm AT).
  Qed.

  Remark lgrp_inv_ok :
    (lvar:(listT (Sprod A nat));l:lgrp)
    (lgrp_interp lvar (lgrp_inv l)) == (iv (lgrp_interp lvar l)).
  Proof.
    Intros.
    Rewrite (lgrp_interp_ok lvar (lgrp_inv l)).
    Rewrite (lgrp_interp_ok lvar l).
    Apply lgrp_inv_ok1.
  Qed.

  Fixpoint lgrp_sort_cons [l:lgrp] : nat -> lgrp :=
    [i:nat]
    Cases l of
    | lgrp_nil => (lgrp_cons i lgrp_nil)
    | (lgrp_cons j l1) =>
      if (blt_nat j i) then (lgrp_cons j (lgrp_sort_cons l1 i)) else
      (lgrp_cons i l)
    | (lgrp_snoc j l1) =>
      if (blt_nat i j) then (lgrp_cons i l) else
      if (blt_nat j i) then (lgrp_snoc j (lgrp_sort_cons l1 i)) else
      l1
    end.

  Fixpoint lgrp_sort_snoc [l:lgrp] : nat -> lgrp :=
    [i:nat]
    Cases l of
    | lgrp_nil => (lgrp_snoc i lgrp_nil)
    | (lgrp_cons j l1) =>
      if (blt_nat i j) then (lgrp_snoc i l) else
      if (blt_nat j i) then (lgrp_cons j (lgrp_sort_snoc l1 i)) else
      l1
    | (lgrp_snoc j l1) =>
      if (blt_nat j i) then (lgrp_snoc j (lgrp_sort_snoc l1 i)) else
                            (lgrp_snoc i l)
    end.

  Remark lgrp_sort_cons_ok1 :
    (lvar:(listT (Sprod A nat));l:lgrp;i:nat)
    (lgrp_interp1 lvar (lgrp_sort_cons l i)) ==
      (op (assoc2 lvar i) (lgrp_interp1 lvar l)).
  Proof.
    Decompose Record AT.
    NewInduction l; Simpl; Intro; Auto.

    NewDestruct (lt_eq_lt_dec n i).
    NewDestruct s.
    Rewrite (lt_imp_blt l0).
    Transitivity
      (op (assoc2 lvar n) (op (assoc2 lvar i) (lgrp_interp1 lvar l))).
    Rewrite <- (IHl i); Reflexivity.
    Rewrite group_assoc.
    Transitivity
      (op (op (assoc2 lvar i) (assoc2 lvar n)) (lgrp_interp1 lvar l));
      Auto.

    Rewrite e; Rewrite (lt_not_refl i); Reflexivity.

    Rewrite (lt_imp_not_blt l0); Reflexivity.

    NewDestruct (lt_eq_lt_dec n i).
    NewDestruct s.
    Rewrite (lt_imp_blt l0).

    Simpl.
    Rewrite (lt_imp_not_blt l0).
    Simpl.
    Rewrite (IHl i).
    Rewrite group_assoc.

    Transitivity
      (op (op (iv (assoc2 lvar n)) (assoc2 lvar i)) (lgrp_interp1 lvar l));
      Auto.

    Rewrite group_assoc; Auto.

    Rewrite e; Rewrite (lt_not_refl i).
    Rewrite group_assoc; Rewrite (group_dx_iv AT); Auto.

    Rewrite (lt_imp_blt l0); Auto.
  Qed.

  Remark lgrp_sort_cons_ok :
    (lvar:(listT (Sprod A nat));l:lgrp;i:nat)
    (lgrp_interp lvar (lgrp_sort_cons l i)) ==
      (op (assoc2 lvar i) (lgrp_interp lvar l)).
  Proof.
    Intros.
    Rewrite (lgrp_interp_ok lvar (lgrp_sort_cons l i)).
    Rewrite (lgrp_interp_ok lvar l).
    Apply lgrp_sort_cons_ok1.
  Qed.

  Remark lgrp_sort_snoc_ok1 :
    (lvar:(listT (Sprod A nat));l:lgrp;i:nat)
    (lgrp_interp1 lvar (lgrp_sort_snoc l i)) ==
      (op (iv (assoc2 lvar i)) (lgrp_interp1 lvar l)).
  Proof.
    Decompose Record AT.
    NewInduction l; Simpl; Intro; Auto.

    NewDestruct (lt_eq_lt_dec n i).
    NewDestruct s.
    Rewrite (lt_imp_blt l0).
    Rewrite (lt_imp_not_blt l0).

    Transitivity
      (op (assoc2 lvar n) (op (iv (assoc2 lvar i)) (lgrp_interp1 lvar l))).
    Rewrite <- (IHl i); Reflexivity.
    Do 2 Rewrite group_assoc; Auto.

    Rewrite e; Rewrite (lt_not_refl i);
      Rewrite group_assoc; Rewrite group_sx_iv; Auto.

    Rewrite (lt_imp_not_blt l0); Rewrite (lt_imp_blt l0); EAuto.

    NewDestruct (lt_eq_lt_dec n i).
    NewDestruct s.
    Rewrite (lt_imp_blt l0).

    Simpl; Rewrite (IHl i); Do 2 Rewrite group_assoc; Auto.

    Rewrite e; Rewrite (lt_not_refl i); Reflexivity.

    Rewrite (lt_imp_not_blt l0); Reflexivity.
  Qed.

  Remark lgrp_sort_snoc_ok :
    (lvar:(listT (Sprod A nat));l:lgrp;i:nat)
    (lgrp_interp lvar (lgrp_sort_snoc l i)) ==
      (op (iv (assoc2 lvar i)) (lgrp_interp lvar l)).
  Proof.
    Intros.
    Rewrite (lgrp_interp_ok lvar (lgrp_sort_snoc l i)).
    Rewrite (lgrp_interp_ok lvar l).
    Apply lgrp_sort_snoc_ok1.
  Qed.

  Fixpoint lgrp_sort_append [l1:lgrp] : lgrp -> lgrp :=
    [l2:lgrp]
    Cases l1 of
    | lgrp_nil => l2
    | (lgrp_cons i l3) => (lgrp_sort_cons (lgrp_sort_append l3 l2) i)
    | (lgrp_snoc i l3) => (lgrp_sort_snoc (lgrp_sort_append l3 l2) i)
    end.

  Remark lgrp_sort_append_ok :
    (lvar:(listT (Sprod A nat));l1,l2:lgrp)
    (lgrp_interp lvar (lgrp_sort_append l1 l2)) ==
      (op (lgrp_interp lvar l1) (lgrp_interp lvar l2)).
  Proof.
    Decompose Record AT.
    NewInduction l1; Simpl; Intros; Auto.

    Rewrite (lgrp_sort_cons_ok lvar (lgrp_sort_append l1 l2) n).
    Rewrite (IHl1 l2).
    NewDestruct l1; Auto.

    Rewrite (lgrp_sort_snoc_ok lvar (lgrp_sort_append l1 l2) n).
    Rewrite (IHl1 l2).
    NewDestruct l1; Auto.
  Qed.

  Fixpoint lgrp_of_expr [a:expr] : lgrp :=
    Cases a of
    | Eid => lgrp_nil
    | (Eop a1 a2) =>
      (lgrp_sort_append (lgrp_of_expr a1) (lgrp_of_expr a2))
    | (Eiv a1) => (lgrp_inv (lgrp_of_expr a1))
    | (Eatom i) => (lgrp_cons i lgrp_nil)
    end.

  Remark lgrp_of_expr_ok :
    (lvar:(listT (Sprod A nat));a:expr)
    (lgrp_interp lvar (lgrp_of_expr a)) == (expr_interp lvar a).
  Proof.
    Decompose Record AT.
    NewInduction a; Simpl; Intros; Auto.
    Rewrite
      (lgrp_sort_append_ok lvar (lgrp_of_expr a1) (lgrp_of_expr a2));
      Auto.
    Rewrite (lgrp_inv_ok lvar (lgrp_of_expr a)); Auto.
  Qed.

  Definition expr_simpl : (listT (Sprod A nat)) -> expr -> A.
    Intros lvar a; Exact (lgrp_interp lvar (lgrp_of_expr a)).
  Defined.

  Lemma expr_simpl_ok :
    (lvar:(listT (Sprod A nat));a:expr)
    (expr_simpl lvar a) == (expr_interp lvar a).
  Proof.
    Intros; Unfold expr_simpl.
    Apply lgrp_of_expr_ok.
  Qed.
End Group_Reflection.


Index
This page has been generated by coqdoc