proposition: Theorem substi_correct_l : forall s x (ts t' : tm), subst x s ts = t' -> substi s x ts t'.
proof: Proof. quickchick. Admitted. Theorem substi_correct_r : forall s x (ts t' : tm), substi s x ts t' -> subst x s ts = t'. Proof. quickchick. Admitted. Reserved Notation "t '-->' t'" (at level 40). Inductive step : tm -> tm -> Prop := | ST_AppAbs : forall x T2 t1 v2, value v2 -> <{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }> | ST_App1 : forall t1 t1' t2, t1 --> t1' -> <{t1 t2}> --> <{t1' t2}> | ST_App2 : forall v1 t2 t2', value v1 -> t2 --> t2' -> <{v1 t2}> --> <{v1 t2'}> | ST_IfTrue : forall t1 t2, <{if true then t1 else t2}> --> t1 | ST_IfFalse : forall t1 t2, <{if false then t1 else t2}> --> t2 | ST_If : forall t1 t1' t2 t3, t1 --> t1' -> <{if t1 then t2 else t3}> --> <{if t1' then t2 else t3}> where "t '-->' t'" := (step t t'). Derive DecOpt for (step t t'). Reserved Notation "Gamma '|--' t '\in' T" (at level 101, t custom stlc, T custom stlc at level 0). Print Grammar constr. Definition t_update (Gamma : string -> option ty) (x : string) (T : ty) (x' : string) : option ty := if (x = x')? then Some T else Gamma x'. Inductive has_type : (string -> option ty) -> tm -> ty -> Prop := | T_Var : forall Gamma x T1, Gamma x = Some T1 -> Gamma |-- x \in T1 | T_Abs : forall Gamma x T1 T2 t1, t_update Gamma x T2 |-- t1 \in T1 -> Gamma |-- \x:T2, t1 \in (T2 -> T1) | T_App : forall T1 T2 Gamma t1 t2, Gamma |-- t1 \in (T2 -> T1) -> Gamma |-- t2 \in T2 -> Gamma |-- t1 t2 \in T1 | T_True : forall Gamma, Gamma |-- true \in Bool | T_False : forall Gamma, Gamma |-- false \in Bool | T_If : forall t1 t2 t3 T1 Gamma, Gamma |-- t1 \in Bool -> Gamma |-- t2 \in T1 -> Gamma |-- t3 \in T1 -> Gamma |-- if t1 then t2 else t3 \in T1 where "Gamma '|--' t '\in' T" := (has_type Gamma t T). Print tm. Definition bindop {A B} (ma : option A) (f : A -> option B) : option B := match ma with | None => None | Some a => f a end. Print ty. Fixpoint type_eqb (T T' : ty) : bool := match T, T' with | Ty_Bool, Ty_Bool => true | Ty_Arrow l r, Ty_Arrow l' r' => (type_eqb l l') && (type_eqb r r') | _, _ => false end. Theorem type_eq_eqb : forall T T', type_eqb T T' = true <-> T = T'. Proof. induction T; intros; destruct T'; simpl in *; split; intros; auto; try discriminate. - rewrite Bool.andb_true_iff in H. destruct H. apply IHT1 in H. apply IHT2 in H0. subst; auto. - injection H as H. subst; simpl; auto. assert (forall T, type_eqb T T = true). + induction T; simpl; auto. rewrite IHT3, IHT4; auto. + do 2 rewrite H. auto. Qed.
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)