| 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.